From 471e777a20cec54a2c0f9b9930479767f6be2d61 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 2 Mar 2011 13:16:06 +0000
Subject: [PATCH] comments
---
src/plugins/e-acsl/visit.ml | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c3e545b2d88..f7c0f46efa6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -41,6 +41,7 @@ extern void eprintf(char * ); \n\
\n\
void e_acsl_fail(char *msg) { eprintf(msg); exit(1); }")
+(* Build a C conditional doing a runtime assertion check. *)
let mk_if acc e p =
(* voidType is incorrect: will be resolved later *)
let f =
@@ -55,6 +56,8 @@ let mk_if acc e p =
let s = Instr(Call(None, f, [ mkString unknown_loc msg ], unknown_loc))in
mkStmt(If(e, mkBlock [ mkStmt s ], mkBlock [], unknown_loc)) :: acc
+(* convert an ACSL named predicate into the opposite C expression (if any).
+ E.g. \true is converted into 0. *)
let rec named_predicate_to_revexp p = match p.content with
| Pfalse -> one ~loc:unknown_loc
| Ptrue -> zero ~loc:unknown_loc
@@ -79,6 +82,11 @@ let rec named_predicate_to_revexp p = match p.content with
| Pfresh _ -> not_yet "\\fresh"
| Psubtype _ -> not_yet "subtyping relation"
+(* ************************************************************************** *)
+(* [convert_*] converts a given ACSL annotation into the corresponding C
+ statement (if any) for runtime assertion checking *)
+(* ************************************************************************** *)
+
let convert_named_predicate acc generate p =
if generate then mk_if acc (named_predicate_to_revexp p) p else acc
@@ -96,8 +104,14 @@ let convert_rooted acc generate (User a | AI(_, a)) =
let convert_before_after acc generate (Before r | After r) =
convert_rooted acc generate r
+(* ************************************************************************** *)
+(* Visitor *)
+(* ************************************************************************** *)
+
+(* local reference to the below visitor and to [do_visit] *)
let first_global = ref true
+(* the main visitor performing e-acsl checking and C code generator *)
class e_acsl_visitor prj generate = object
inherit Visitor.generic_frama_c_visitor
--
GitLab