From 5a0ab6a0a12c3f52dc369577f0dd9ba299962446 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 13 Mar 2013 12:40:25 +0000
Subject: [PATCH] fixed again according to kernel changes and fixed
compatibility with the -no-obj mode
---
src/plugins/e-acsl/mpz.ml | 4 +++-
src/plugins/e-acsl/pre_analysis.ml | 17 ++++++++++++-----
src/plugins/e-acsl/translate.ml | 18 +++++++++++++-----
src/plugins/e-acsl/typing.ml | 2 +-
src/plugins/e-acsl/visit.ml | 13 ++++++++-----
5 files changed, 37 insertions(+), 17 deletions(-)
diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index 29cb7ad11a1..6f1b0854831 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -47,7 +47,9 @@ let get_set_suffix_and_arg e =
else
match Cil.unrollType ty with
| TInt(IChar, _) ->
- (if Cil.theMachine.Cil.char_is_unsigned then "_ui" else "_si"), [ e ]
+ (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
+ else "_si"),
+ [ e ]
| TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
"_ui", [ e ]
| TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 02f7eab9164..00fd5d7a686 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -41,11 +41,18 @@ let init_mpz () =
(* ********************************************************************** *)
let get_rte_by_stmt =
- Dynamic.get
- ~plugin:"RteGen"
- "stmt_annotations"
- (Datatype.func2 Kernel_function.ty Stmt.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
+ try
+ Dynamic.get
+ ~plugin:"RteGen"
+ "stmt_annotations"
+ (Datatype.func2 Kernel_function.ty Stmt.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
+ with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
+ ->
+ Options.warning "@[@[cannot run RTE:@ %s.@]@ \
+Ignoring potential runtime errors in annotations."
+ (Printexc.to_string exn);
+ fun _ _ -> []
module Env: sig
val default_varinfos: Varinfo.Set.t option -> Varinfo.Set.t
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index aa6a48ae26e..195ec761fbc 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -632,11 +632,19 @@ let assumes_predicate bhv =
bhv.b_assumes
let get_rte =
- Dynamic.get
- ~plugin:"RteGen"
- "exp_annotations"
- (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
+ try
+ Dynamic.get
+ ~plugin:"RteGen"
+ "exp_annotations"
+ (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
+ with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
+ ->
+ Options.warning "@[@[cannot run RTE:@ %s.@]@ \
+Ignoring potential runtime errors in annotations."
+ (Printexc.to_string exn);
+ fun _ _ _ -> []
+
let rec translate_named_predicate kf _kinstr ?(rte=true) env p =
Typing.type_named_predicate ~must_clear:rte p;
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index cb45ff77835..d2f2739c8a4 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -213,7 +213,7 @@ let size_of ty =
try int_to_interv (Cil.sizeOf_int ty)
with Cil.SizeOfError _ -> eacsl_typ_of_typ Cil.ulongLongType
-let align_of ty = int_to_interv (Cil.alignOf_int ty)
+let align_of ty = int_to_interv (Cil.bytesAlignOf ty)
type offset_ty = Ty_no_offset | Ty_field of eacsl_typ | Ty_index of eacsl_typ
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 713538f476e..f13f4f84f42 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -24,11 +24,14 @@ open Cil_types
open Cil_datatype
let get_rte_by_stmt =
- Dynamic.get
- ~plugin:"RteGen"
- "stmt_annotations"
- (Datatype.func2 Kernel_function.ty Stmt.ty
- (let module L = Datatype.List(Code_annotation) in L.ty))
+ try
+ Dynamic.get
+ ~plugin:"RteGen"
+ "stmt_annotations"
+ (Datatype.func2 Kernel_function.ty Stmt.ty
+ (let module L = Datatype.List(Code_annotation) in L.ty))
+ with _ ->
+ fun _ _ -> []
(* move all labels of [stmt] onto [new_stmt] *)
let move_labels env stmt new_stmt =
--
GitLab