From 87c81ea1510b3dedfff588dc95a117f4fbc2af69 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 10 Jun 2014 16:36:04 +0200
Subject: [PATCH] [e-acsl] improve a bit the Frama-C script of the demo
---
src/plugins/e-acsl/demo/script.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/demo/script.ml b/src/plugins/e-acsl/demo/script.ml
index 37558dbeaaa..2c078362659 100644
--- a/src/plugins/e-acsl/demo/script.ml
+++ b/src/plugins/e-acsl/demo/script.ml
@@ -44,12 +44,12 @@ module Ppt_line =
exception Found of Property.t * int
-let search_assert kf =
+let search_assert_or_invariant kf =
try
Annotations.iter_all_code_annot
(fun stmt _ a ->
match a.annot_content with
- | AAssert(_, p) ->
+ | AAssert(_, p) | AInvariant(_, _, p) ->
let line = Ppt_line.get () in
if (fst (p.loc)).Lexing.pos_lnum = line then
raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
@@ -88,10 +88,10 @@ let search_requires kf =
kf
let search kf = match Ppt_name.get () with
- | "" | "Assertion" -> search_assert kf
+ | "" | "Assertion" | "Invariant" -> search_assert_or_invariant kf
| "Precondition" -> search_requires kf
| "Postcondition" -> search_ensures kf
- | _ -> assert false
+ | s -> abort "unknown property %s" s
(* ************************************************************************** *)
(* Emitting status "invalid" for the property *)
--
GitLab