File tree Expand file tree Collapse file tree
english/acsl-logic-definitions
french/acsl-logic-definitions Expand file tree Collapse file tree Original file line number Diff line number Diff line change 181181program, for any input, its observable behavior is the same with or
182182without the ghost code.
183183
184-
185- \begin {Warning }
186- Before Frama-C 21 Scandium, most of these properties were not
187- verified by the Frama-C kernel. Thus, if we work with a previous
188- version, we have to ensure that they are verified ourselves.
189- \end {Warning }
190-
191-
192184If some of these properties are not verified, it would mean that
193185the ghost code can change the behavior of the verified program.
194186Let us have a closer look to each of these constraints.
Original file line number Diff line number Diff line change 188188avec ou sans le code fantôme.
189189
190190
191- \begin {Warning }
192- Avant Frama-C 21 Scandium, la plupart de ces propriétés n'étaient pas vérifiées
193- par le noyau de Frama-C. Par conséquent, si l'on travaille avec une version
194- antérieure, il faut s'assurer soi-même que ces propriétés sont vérifiées.
195- \end {Warning }
196-
197-
198191Si certaines de ces propriétés ne sont pas vérifiées, cela voudrait dire que le
199192code fantôme peut changer le comportement du programme vérifié. Analysons de plus
200193prêt chacune de ces contraintes.
You can’t perform that action at this time.
0 commit comments