diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 64a0142c4f5a63aa2842858db8ec8c9b12698818..731e28b1da14b733e369c8601618ff5fd2196e87 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,6 +1,7 @@
Version number Date of release Notes
============== =============== =====
-23.0 (Vanadium) 2021, June 28
+23.1 (Vanadium) 2021, July 20
+23.0 (Vanadium) 2021, July 7
22.0 (Titanium) 2020, November 17
21.1 (Scandium) 2020, June 25 Bugs fixed
21.0 (Scandium) 2020, June 11
diff --git a/Changelog b/Changelog
index 4f057090fcd8e5dc3e7e5d0ded399971050cc307..e797181966e498d749f96bc11d03023010523273 100644
--- a/Changelog
+++ b/Changelog
@@ -25,6 +25,10 @@ o Kernel [2021-06-10] New module Cil_builder, simplifies C and ACSL code
o Ptests [2021-06-03] Add new PLUGIN directive and new predefined macros.
- Eva [2021-05-11] Support for ACSL predicate \is_infinite.
+###################################
+Open Source Release 23.1 (Vanadium)
+###################################
+
###################################
Open Source Release 23.0 (Vanadium)
###################################
diff --git a/VERSION b/VERSION
index 1d37314c457169b4e9ce45deac798ae467fbc459..930e9e656373bd9c3a4939e14ebdad9bf7daaca9 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-23.0+dev
+23.1+dev
diff --git a/opam/opam b/opam/opam
index bba7a550a8ca6624b6abcd1696a328c1bfa954e8..4ca43003a0b54d07e8ae15487b96b8e804b582aa 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "23.0"
+version: "23.1"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -99,7 +99,7 @@ install: [
]
run-test: [
- [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] { arch != "ppc64" }
+ [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
# tests are disabled on PPC64 due to floating-point oracle differences
# (some ULPs in libc trigonometric functions) and due to the lack of
# available hardware to test them locally
@@ -115,12 +115,12 @@ depends: [
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
"conf-time" { with-test }
- "ocaml" { >= "4.08.1" }
+ "ocaml" { >= "4.08.1" & < "4.13.0" }
"ocamlfind" # needed beyond build stage, used by -load-module
"ocamlgraph" { >= "1.8.8" }
"why3" { >= "1.4.0" & < "1.5~" }
- "yojson"
- "zarith"
+ "yojson" {>= "1.6.0"}
+ "zarith" {>= "1.5"}
]
depopts: [
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index c05704c94c67baf0658a7209701a7be811bfffd2..6b448f789441d6b8d95e5a5a1acd19e4d2ded92c 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,12 +25,6 @@
Plugin E-ACSL <next-release>
############################
--* E-ACSL [2021-07-19] Fix crash occurring when two or more successive
- logic coercions were done in a term (frama-c/e-acsl#172).
--* E-ACSL [2021-07-19] Fix crash when raising some user errors
- (frama-c/e-acsl#170).
--* E-ACSL [2021-07-16] Fix crash when using some built-in labels
- (frama-c/e-acsl#173).
- E-ACSL [2021-07-06] Add support for the extended quantifier \sum.
-* E-ACSL [2021-06-22] Fix a crash that occured when using certain
combinations of nested blocks and annotations.
@@ -40,6 +34,19 @@ Plugin E-ACSL <next-release>
range indices (frama-c/e-acsl#148).
-* E-ACSL [2021-06-04] Do not translate contracts of E-ACSL built-ins.
+#############################
+Plugin E-ACSL 23.1 (Vanadium)
+#############################
+
+-* E-ACSL [2021-07-19] Fix crash occurring when two or more successive
+ logic coercions were done in a term (frama-c/e-acsl#172).
+-* E-ACSL [2021-07-19] Fix crash when raising some user errors
+ (frama-c/e-acsl#170).
+-* E-ACSL [2021-07-16] Fix crash when using some built-in labels
+ (frama-c/e-acsl#173).
+-* E-ACSL [2021-07-13] Fix crash when encountering a GMP value in a loop
+ variant (frama-c/e-acsl#169).
+
#############################
Plugin E-ACSL 23.0 (Vanadium)
#############################
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 656f790c6b03964797ddc44cf27dd361cb7cb684..c6d6e726ba7e5f183f42551b3bba4e57472811ad 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -48,32 +48,37 @@ let handle_annotations env kf stmt =
| Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
(* Loop variant, save the current value of the variant *)
let stmts, env, variant =
- match Env.top_loop_variant env with
- | Some (t, measure_opt) ->
- let env = Env.set_annotation_kind env Smart_stmt.Variant in
- let env = Env.push env in
- Typing.type_term ~use_gmp_opt:true t;
- let ty = Typing.get_typ t in
- let e, env = !term_to_exp_ref kf env t in
- let vi_old, e_old, env =
- Env.new_var
- ~loc
- ~scope:Varname.Function
- ~name:"old_variant"
- env
- kf
- (Some t)
- ty
- (fun _ _ -> [])
- in
- let stmt =
- Smart_stmt.assigns ~loc ~result:(Cil.var vi_old) e
- in
- let blk, env =
- Env.pop_and_get env stmt ~global_clear:false Env.Middle
- in
- Smart_stmt.block_stmt blk :: stmts, env, Some (t, e_old, measure_opt)
- | None -> stmts, env, None
+ Error.handle
+ (fun (stmts, env, _) ->
+ match Env.top_loop_variant env with
+ | Some (t, measure_opt) ->
+ let env = Env.set_annotation_kind env Smart_stmt.Variant in
+ let env = Env.push env in
+ Typing.type_term ~use_gmp_opt:true t;
+ let ty = Typing.get_typ t in
+ if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
+ let e, env = !term_to_exp_ref kf env t in
+ let vi_old, e_old, env =
+ Env.new_var
+ ~loc
+ ~scope:Varname.Function
+ ~name:"old_variant"
+ env
+ kf
+ (Some t)
+ ty
+ (fun _ _ -> [])
+ in
+ let stmt =
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi_old) e
+ in
+ let blk, env =
+ Env.pop_and_get env stmt ~global_clear:false Env.Middle
+ in
+ let stmts = Smart_stmt.block_stmt blk :: stmts in
+ stmts, env, Some (t, e_old, measure_opt)
+ | None -> stmts, env, None)
+ (stmts, env, None)
in
(* Auxiliary function to generate variant and invariant checks *)
let rec aux (stmts, env) = function
@@ -118,14 +123,23 @@ let handle_annotations env kf stmt =
stmts, env
| Some (t, e_old, None) ->
let env = Env.push env in
- Typing.type_term ~use_gmp_opt:true t;
- let e, env = !term_to_exp_ref kf env t in
+ let t_old = Logic_utils.expr_to_term e_old in
+ let variant_pos =
+ Logic_const.prel ~loc (Rge, t_old, Logic_const.tinteger ~loc 0)
+ in
+ Typing.type_named_predicate ~must_clear:true variant_pos;
+ let variant_pos_e, env = !predicate_to_exp_ref kf env variant_pos in
let msg1 =
Format.asprintf
"(old %a) %a 0"
Printer.pp_term t
Printer.pp_relation Rge
in
+ let variant_dec =
+ Logic_const.prel ~loc (Rgt, t_old, t)
+ in
+ Typing.type_named_predicate ~must_clear:true variant_dec;
+ let variant_dec_e, env = !predicate_to_exp_ref kf env variant_dec in
let msg2 =
Format.asprintf
"(old %a) > %a"
@@ -140,14 +154,14 @@ let handle_annotations env kf stmt =
~pred_kind:Assert
Smart_stmt.Variant
kf
- (Cil.mkBinOp ~loc Ge e_old (Cil.zero ~loc));
+ variant_pos_e;
Smart_stmt.runtime_check_with_msg
~loc
msg2
~pred_kind:Assert
Smart_stmt.Variant
kf
- (Cil.mkBinOp ~loc Gt e_old e)
+ variant_dec_e
]
in
let blk, env =
diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.c
similarity index 82%
rename from src/plugins/e-acsl/tests/constructs/decrease.i
rename to src/plugins/e-acsl/tests/constructs/decrease.c
index 4bb96675366a34026d543101466313a8add9cb9e..4e32701dbebbabe29db2ce924d45c7f7df62d1e4 100644
--- a/src/plugins/e-acsl/tests/constructs/decrease.i
+++ b/src/plugins/e-acsl/tests/constructs/decrease.c
@@ -2,6 +2,8 @@
STDOPT: +"-eva-unroll-recursive-calls 10 -eva-slevel 7"
*/
+#include <stddef.h>
+
// Test that the last iteration of the variant can be negative
int f(int x) {
/*@ loop variant x; */
@@ -35,6 +37,18 @@ int fact(int n) {
return result;
}
+// Test GMP variant
+/*@ requires n <= 20; */
+size_t fact2(size_t n) {
+ size_t result = n;
+ /*@ loop invariant 1 <= i < n;
+ loop variant n - i; */
+ for (size_t i = 1UL ; i < (n - 1UL) ; i++) {
+ result *= (n - i);
+ }
+ return result;
+}
+
// Test decreases on recursive function
/*@ decreases n; */
int fib(int n) {
@@ -71,6 +85,9 @@ int main() {
int fact7 = fact(7);
//@ assert fact7 == 5040;
+ size_t fact18 = fact2(18);
+ //@ assert fact18 == 6402373705728000UL;
+
int fib7 = fib(7);
//@ assert fib7 == 13;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle
index 2a909408ab28551a31c8128f578c384ab0e246df..677ba8aacfddbb93a3fc0644b971456fc44ec92f 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle
@@ -1,11 +1,16 @@
[e-acsl] beginning translation.
-[e-acsl] tests/constructs/decrease.i:50: Warning:
+[e-acsl] tests/constructs/decrease.c:45: Warning:
+ E-ACSL construct `loop variant using GMP' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/constructs/decrease.c:64: Warning:
E-ACSL construct `decreases clause' is not yet supported.
Ignoring annotation.
-[e-acsl] tests/constructs/decrease.i:47: Warning:
+[e-acsl] tests/constructs/decrease.c:61: Warning:
E-ACSL construct `decreases clause' is not yet supported.
Ignoring annotation.
-[e-acsl] tests/constructs/decrease.i:40: Warning:
+[e-acsl] tests/constructs/decrease.c:54: Warning:
E-ACSL construct `decreases clause' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/constructs/decrease.c:89: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
index 116816df289b37cce0dcf9fe63c4b5fe6b748abf..f7b974205400d3cc2e7b01e80412975f1a7a9a96 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
@@ -12,9 +12,10 @@ int f(int x)
if (! (x >= 0)) break;
x -= 2;
__e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","f",
- "(old x) \342\211\245 0","tests/constructs/decrease.i",8);
+ "(old x) \342\211\245 0","tests/constructs/decrease.c",
+ 10);
__e_acsl_assert(__gen_e_acsl_old_variant > x,1,"Variant","f",
- "(old x) > x","tests/constructs/decrease.i",8);
+ "(old x) > x","tests/constructs/decrease.c",10);
}
return x;
}
@@ -36,7 +37,7 @@ int g(int x)
int __gen_e_acsl_lexico_2;
__gen_e_acsl_lexico_2 = __gen_e_acsl_lexico(__gen_e_acsl_old_variant,x);
__e_acsl_assert(__gen_e_acsl_lexico_2,1,"Variant","g",
- "lexico(old x, x)","tests/constructs/decrease.i",19);
+ "lexico(old x, x)","tests/constructs/decrease.c",21);
}
}
return x;
@@ -50,7 +51,7 @@ int fact(int n)
int __gen_e_acsl_old_variant;
int result = n;
__e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
- "tests/constructs/decrease.i",29);
+ "tests/constructs/decrease.c",31);
/*@ loop invariant n ≥ 1;
loop variant n; */
while (1) {
@@ -59,12 +60,43 @@ int fact(int n)
result *= n - 1;
n --;
__e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
- "tests/constructs/decrease.i",29);
+ "tests/constructs/decrease.c",31);
__e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","fact",
- "(old n) \342\211\245 0","tests/constructs/decrease.i",
- 31);
+ "(old n) \342\211\245 0","tests/constructs/decrease.c",
+ 33);
__e_acsl_assert(__gen_e_acsl_old_variant > n,1,"Variant","fact",
- "(old n) > n","tests/constructs/decrease.i",31);
+ "(old n) > n","tests/constructs/decrease.c",33);
+ }
+ return result;
+}
+
+/*@ requires n ≤ 20; */
+size_t __gen_e_acsl_fact2(size_t n);
+
+size_t fact2(size_t n)
+{
+ size_t result = n;
+ {
+ size_t i = 1UL;
+ {
+ int __gen_e_acsl_and;
+ if (1UL <= i) __gen_e_acsl_and = i < n; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,1,"Invariant","fact2","1 <= i < n",
+ "tests/constructs/decrease.c",44);
+ }
+ /*@ loop invariant 1 ≤ i < n;
+ loop variant n - i; */
+ while (i < n - 1UL) {
+ result *= n - i;
+ {
+ int __gen_e_acsl_and_2;
+ i += (size_t)1;
+ if (1UL <= i) __gen_e_acsl_and_2 = i < n;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,1,"Invariant","fact2",
+ "1 <= i < n","tests/constructs/decrease.c",44);
+ }
+ }
}
return result;
}
@@ -132,43 +164,48 @@ int main(void)
int __retres;
int f10 = f(10);
__e_acsl_assert(f10 == -2,1,"Assertion","main","f10 == -2",
- "tests/constructs/decrease.i",63);
+ "tests/constructs/decrease.c",77);
/*@ assert f10 ≡ -2; */ ;
int f7 = f(7);
__e_acsl_assert(f7 == -1,1,"Assertion","main","f7 == -1",
- "tests/constructs/decrease.i",65);
+ "tests/constructs/decrease.c",79);
/*@ assert f7 ≡ -1; */ ;
int g10 = g(10);
__e_acsl_assert(g10 == -2,1,"Assertion","main","g10 == -2",
- "tests/constructs/decrease.i",67);
+ "tests/constructs/decrease.c",81);
/*@ assert g10 ≡ -2; */ ;
int g7 = g(7);
__e_acsl_assert(g7 == -1,1,"Assertion","main","g7 == -1",
- "tests/constructs/decrease.i",69);
+ "tests/constructs/decrease.c",83);
/*@ assert g7 ≡ -1; */ ;
int fact7 = __gen_e_acsl_fact(7);
__e_acsl_assert(fact7 == 5040,1,"Assertion","main","fact7 == 5040",
- "tests/constructs/decrease.i",72);
+ "tests/constructs/decrease.c",86);
/*@ assert fact7 ≡ 5040; */ ;
+ size_t fact18 = __gen_e_acsl_fact2((unsigned long)18);
+ __e_acsl_assert(fact18 == 6402373705728000UL,1,"Assertion","main",
+ "fact18 == 6402373705728000UL",
+ "tests/constructs/decrease.c",89);
+ /*@ assert fact18 ≡ 6402373705728000UL; */ ;
int fib7 = __gen_e_acsl_fib(7);
__e_acsl_assert(fib7 == 13,1,"Assertion","main","fib7 == 13",
- "tests/constructs/decrease.i",75);
+ "tests/constructs/decrease.c",92);
/*@ assert fib7 ≡ 13; */ ;
int even7 = __gen_e_acsl_even(7);
__e_acsl_assert(even7 == 0,1,"Assertion","main","even7 == 0",
- "tests/constructs/decrease.i",78);
+ "tests/constructs/decrease.c",95);
/*@ assert even7 ≡ 0; */ ;
int even10 = __gen_e_acsl_even(10);
__e_acsl_assert(even10 == 1,1,"Assertion","main","even10 == 1",
- "tests/constructs/decrease.i",80);
+ "tests/constructs/decrease.c",97);
/*@ assert even10 ≡ 1; */ ;
int odd7 = __gen_e_acsl_odd(7);
__e_acsl_assert(odd7 == 1,1,"Assertion","main","odd7 == 1",
- "tests/constructs/decrease.i",82);
+ "tests/constructs/decrease.c",99);
/*@ assert odd7 ≡ 1; */ ;
int odd10 = __gen_e_acsl_odd(10);
__e_acsl_assert(odd10 == 0,1,"Assertion","main","odd10 == 0",
- "tests/constructs/decrease.i",84);
+ "tests/constructs/decrease.c",101);
/*@ assert odd10 ≡ 0; */ ;
__retres = 0;
return __retres;
@@ -180,7 +217,7 @@ int __gen_e_acsl_even(int n)
{
int __retres;
__e_acsl_assert(n >= 0,1,"Precondition","even","n >= 0",
- "tests/constructs/decrease.i",48);
+ "tests/constructs/decrease.c",62);
__retres = even(n);
return __retres;
}
@@ -191,7 +228,7 @@ int __gen_e_acsl_odd(int n)
{
int __retres;
__e_acsl_assert(n >= 0,1,"Precondition","odd","n >= 0",
- "tests/constructs/decrease.i",54);
+ "tests/constructs/decrease.c",68);
__retres = odd(n);
return __retres;
}
@@ -204,12 +241,22 @@ int __gen_e_acsl_fib(int n)
return __retres;
}
+/*@ requires n ≤ 20; */
+size_t __gen_e_acsl_fact2(size_t n)
+{
+ size_t __retres;
+ __e_acsl_assert(n <= 20UL,1,"Precondition","fact2","n <= 20",
+ "tests/constructs/decrease.c",41);
+ __retres = fact2(n);
+ return __retres;
+}
+
/*@ requires n ≤ 12; */
int __gen_e_acsl_fact(int n)
{
int __retres;
__e_acsl_assert(n <= 12,1,"Precondition","fact","n <= 12",
- "tests/constructs/decrease.i",26);
+ "tests/constructs/decrease.c",28);
__retres = fact(n);
return __retres;
}
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index afef9d75caeb521a6391a36bfd4edc1ed8879b73..21944be46f3999616ea7d7a829deae9225d730fc 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,11 @@
Plugin WP <next-release>
#########################
+
+#########################
+Plugin WP 23.1 (Vanadium)
+#########################
+
- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
Adds the options -wp-declaration-terminate and
-wp-frama-c-stdlib to claims that external functions
@@ -37,6 +42,7 @@ Plugin WP <next-release>
option -wp-smoke-dead-assumes
- TIP [2021-05-31] Generalized Overflow tactic
+- WP [2021-07-15] Fix a crash related to opaque structures memory typing
#########################
Plugin WP 23.0 (Vanadium)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index abf67a6cb7c4af3ce67261a735ecfe22503268ff..5e19be9715d051d8624679c28e4046d669481044 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -118,7 +118,6 @@ let pointer = Context.create "MemTyped.pointer"
type chunk =
| M_int of Ctypes.c_int
- | M_char
| M_f32
| M_f64
| M_pointer
@@ -141,7 +140,6 @@ struct
| SInt64 -> 8
let rank = function
- | M_char -> -1
| M_int i -> int_rank i
| M_f32 -> 9
| M_f64 -> 10
@@ -150,8 +148,8 @@ struct
| T_init -> 13
let hash = rank
let name = function
+ | M_int i when Ctypes.is_char i -> "Mchar"
| M_int _ -> "Mint"
- | M_char -> "Mchar"
| M_f32 -> "Mf32"
| M_f64 -> "Mf64"
| M_pointer -> "Mptr"
@@ -164,14 +162,14 @@ struct
| M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
| m -> Format.pp_print_string fmt (name m)
let val_of_chunk = function
- | M_int _ | M_char -> L.Int
+ | M_int _ -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
| M_f64 -> Cfloat.tau_of_float Ctypes.Float64
| M_pointer -> t_addr
| T_alloc -> L.Int
| T_init -> L.Bool
let tau_of_chunk = function
- | M_int _ | M_char -> L.Array(t_addr,L.Int)
+ | M_int _ -> L.Array(t_addr,L.Int)
| M_pointer -> L.Array(t_addr,t_addr)
| M_f32 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float32)
| M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
@@ -190,11 +188,10 @@ type loc = term (* of type addr *)
(* --- Utilities on locations --- *)
(* -------------------------------------------------------------------------- *)
-let m_int i = if Ctypes.is_char i then M_char else M_int i
let m_float = function Float32 -> M_f32 | Float64 -> M_f64
let rec footprint = function
- | C_int i -> Heap.Set.singleton (m_int i)
+ | C_int i -> Heap.Set.singleton (M_int i)
| C_float f -> Heap.Set.singleton (m_float f)
| C_pointer _ -> Heap.Set.singleton M_pointer
| C_array a -> footprint (object_of a.arr_element)
@@ -215,7 +212,7 @@ and all_value_chunks () =
[ Ctypes.CBool ;
SInt8 ; UInt8 ; SInt16 ; UInt16 ; SInt32 ; UInt32 ; SInt64 ; UInt64 ]
in
- Heap.Set.of_list (M_pointer :: M_char :: M_f32 :: M_f64 :: ints)
+ Heap.Set.of_list (M_pointer :: M_f32 :: M_f64 :: ints)
let init_footprint _ _ = Heap.Set.singleton T_init
let value_footprint obj _l = footprint obj
@@ -482,8 +479,10 @@ module STRING = WpContext.Generator(LITERAL)
let name = prefix ^ "_literal" in
let i = Lang.freshvar ~basename:"i" L.Int in
let c = Cstring.char_at cst (e_var i) in
- let addr = shift (a_global base) (C_int (Ctypes.c_char ())) (e_var i) in
- let m = Lang.freshvar ~basename:"mchar" (Chunk.tau_of_chunk M_char) in
+ let ikind = Ctypes.c_char () in
+ let addr = shift (a_global base) (C_int ikind) (e_var i) in
+ let m =
+ Lang.freshvar ~basename:"mchar" (Chunk.tau_of_chunk (M_int ikind)) in
let m_sconst = F.p_call p_sconst [e_var m] in
let v = F.e_get (e_var m) addr in
let read = F.p_equal c v in
@@ -980,7 +979,6 @@ module ChunkContent = WpContext.Generator(Chunk)
type data = lfun
let int_kind = function
- | M_char -> Ctypes.c_char ()
| M_int k -> k
| _ -> failwith "MemTyped asked constraint for non int type"
@@ -1005,7 +1003,7 @@ module ChunkContent = WpContext.Generator(Chunk)
end)
let is_chunk sigma = function
- | M_int _ | M_char as m ->
+ | M_int _ as m ->
F.p_call (ChunkContent.get m) [ Sigma.value sigma m ]
| _ ->
p_true
@@ -1034,7 +1032,7 @@ struct
let to_region_pointer l = 0,l
let of_region_pointer _ _ l = l
- let load_int sigma i l = F.e_get (Sigma.value sigma (m_int i)) l
+ let load_int sigma i l = F.e_get (Sigma.value sigma (M_int i)) l
let load_float sigma f l = F.e_get (Sigma.value sigma (m_float f)) l
let load_pointer sigma _t l = F.e_get (Sigma.value sigma M_pointer) l
@@ -1061,7 +1059,7 @@ struct
let updated sigma c l v = c , F.e_set (Sigma.value sigma c) l v
- let store_int sigma i l v = updated sigma (m_int i) l v
+ let store_int sigma i l v = updated sigma (M_int i) l v
let store_float sigma f l v = updated sigma (m_float f) l v
let store_pointer sigma _ty l v = updated sigma M_pointer l v
@@ -1156,7 +1154,7 @@ let frame sigma =
in
wellformed_frame p_linked T_alloc @
wellformed_frame p_cinits T_init @
- wellformed_frame p_sconst M_char @
+ wellformed_frame p_sconst (M_int (Ctypes.c_char ())) @
wellformed_frame p_framed M_pointer
let alloc sigma xs =
diff --git a/src/plugins/wp/tests/wp_acsl/opaque_struct.i b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
index c1e457182f2950047598a6d1005b47d07461e5da..40b9c7626f9f91ebffc6aa1c616967458e73b3c0 100644
--- a/src/plugins/wp/tests/wp_acsl/opaque_struct.i
+++ b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
@@ -1,3 +1,10 @@
+/* run.config
+ OPT: -wp-rte
+*/
+/* run.config_qualif
+ OPT: -wp-rte
+*/
+
struct S;
extern struct S S1;
@@ -63,3 +70,14 @@ void assigns_effect(int* p, float* q, char* c, struct S *a){
//@ check fail: *q == \at(*q, Pre);
//@ check succeed: *c == \at(*c, Pre);
}
+
+// regression on MemTyped chunk typing
+
+void use(struct S * s);
+
+//@ requires \valid(uc) && \valid_read(sc) ;
+void chunk_typing(unsigned char* uc, signed char* sc){
+ struct S* s ;
+ *uc = *sc ;
+ use(s) ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index 519985dbf06721b87bb7f9823c5b53859268672c..ea7df3161832b757ba0905c7e57c740a8f29742a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -1,7 +1,14 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
+[rte] annotating function assigned_via_pointer
+[rte] annotating function assigns
+[rte] annotating function assigns_effect
+[rte] annotating function chunk_typing
+[rte] annotating function initialized_assigns
+[rte] annotating function uninitialized_assigns
+[kernel:annot:missing-spec] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Neither code nor specification for function use, generating default assigns from the prototype
------------------------------------------------------------
Axiomatic 'test'
------------------------------------------------------------
@@ -24,38 +31,46 @@ Prove: 0<=BytesLength_of_S1_S
Function assigned_via_pointer
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 53):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 60):
+Let a = havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S).
+Let a_1 = havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S).
+Let a_2 = havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S).
+Let a_3 = havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S).
+Let a_4 = havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S).
+Let a_5 = havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S).
+Let a_6 = havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S).
+Let a_7 = havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S).
+Let a_8 = havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S).
Assume {
+ Type: is_bool_chunk(Mint_0) /\ is_sint16_chunk(Mint_3) /\
+ is_sint32_chunk(Mint_5) /\ is_sint64_chunk(Mint_7) /\
+ is_sint8_chunk(Mchar_0) /\ is_uint16_chunk(Mint_2) /\
+ is_uint32_chunk(Mint_4) /\ is_uint64_chunk(Mint_6) /\
+ is_uint8_chunk(Mint_1) /\ is_bool_chunk(a) /\ is_sint16_chunk(a_1) /\
+ is_sint32_chunk(a_2) /\ is_sint64_chunk(a_3) /\ is_sint8_chunk(a_4) /\
+ is_uint16_chunk(a_5) /\ is_uint32_chunk(a_6) /\ is_uint64_chunk(a_7) /\
+ is_uint8_chunk(a_8).
(* Heap *)
Type: (region(p.base) <= 0) /\ framed(Mptr_0) /\ sconst(Mchar_0).
}
-Prove: EqS1_S(Load_S1_S(p, havoc(Mchar_undef_0, Mchar_0, p, Length_of_S1_S),
- havoc(Mint_undef_0, Mint_0, p, Length_of_S1_S),
- havoc(Mint_undef_1, Mint_1, p, Length_of_S1_S),
- havoc(Mint_undef_2, Mint_2, p, Length_of_S1_S),
- havoc(Mint_undef_3, Mint_3, p, Length_of_S1_S),
- havoc(Mint_undef_4, Mint_4, p, Length_of_S1_S),
- havoc(Mint_undef_5, Mint_5, p, Length_of_S1_S),
- havoc(Mint_undef_6, Mint_6, p, Length_of_S1_S),
- havoc(Mint_undef_7, Mint_7, p, Length_of_S1_S),
- havoc(Mint_undef_8, Mint_8, p, Length_of_S1_S),
+Prove: EqS1_S(Load_S1_S(p, a, a_8, a_4, a_5, a_1, a_6, a_2, a_7, a_3,
havoc(Mf32_undef_0, Mf32_0, p, Length_of_S1_S),
havoc(Mf64_undef_0, Mf64_0, p, Length_of_S1_S),
havoc(Mptr_undef_0, Mptr_0, p, Length_of_S1_S)),
- Load_S1_S(p, Mchar_0, Mint_0, Mint_1, Mint_2, Mint_3, Mint_4,
- Mint_5, Mint_6, Mint_7, Mint_8, Mf32_0, Mf64_0, Mptr_0)).
+ Load_S1_S(p, Mint_0, Mint_1, Mchar_0, Mint_2, Mint_3, Mint_4,
+ Mint_5, Mint_6, Mint_7, Mf32_0, Mf64_0, Mptr_0)).
------------------------------------------------------------
------------------------------------------------------------
Function assigns
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 17):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 24):
Prove: EqS1_S(S1_0, S1_1).
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 18):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 25):
Prove: true.
------------------------------------------------------------
@@ -63,22 +78,24 @@ Prove: true.
Function assigns_effect
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 62):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 69):
Let x = Mint_0[p].
-Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S)[p].
+Let a_1 = havoc(Mint_undef_0, Mint_0, a, Length_of_S1_S).
+Let a_2 = a_1[p].
Assume {
- Type: is_sint32(x) /\ is_sint32(a_1).
+ Type: is_sint32_chunk(Mint_0) /\ is_sint32(x) /\ is_sint32_chunk(a_1) /\
+ is_sint32(a_2).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(p.base) <= 0).
(* Pre-condition *)
Have: separated(a, Length_of_S1_S, c, 1).
}
-Prove: a_1 = x.
+Prove: a_2 = x.
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 63):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 70):
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
@@ -91,24 +108,39 @@ Prove: of_f32(havoc(Mf32_undef_0, Mf32_0, a, Length_of_S1_S)[q])
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 64):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 71):
Let x = Mchar_0[c].
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S)[c].
+Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, Length_of_S1_S).
+Let a_2 = a_1[c].
Assume {
- Type: is_sint8(x) /\ is_sint8(a_1).
+ Type: is_sint8_chunk(Mchar_0) /\ is_sint8(x) /\ is_sint8_chunk(a_1) /\
+ is_sint8(a_2).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: separated(a, Length_of_S1_S, c, 1).
}
-Prove: a_1 = x.
+Prove: a_2 = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function chunk_typing
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/opaque_struct.i, line 81):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/opaque_struct.i, line 81):
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function initialized_assigns
------------------------------------------------------------
-Goal Check 'fails' (file tests/wp_acsl/opaque_struct.i, line 31):
+Goal Check 'fails' (file tests/wp_acsl/opaque_struct.i, line 38):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -124,7 +156,7 @@ Prove: IsInit_S1_S(p, a).
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 32):
+Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 39):
Let x = p.base.
Assume {
(* Heap *)
@@ -139,7 +171,7 @@ Prove: 0 <= (BytesLength_of_S1_S * (Malloc_0[x] / Length_of_S1_S)).
Function uninitialized_assigns
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 47):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 54):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -153,7 +185,7 @@ Prove: !IsInit_S1_S(p, a).
------------------------------------------------------------
-Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 48):
+Goal Check 'fail' (file tests/wp_acsl/opaque_struct.i, line 55):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -166,17 +198,17 @@ Assume {
Prove: IsInit_S1_S(p, a).
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:31: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
-[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:64: Warning:
Memory model hypotheses for function 'assign':
/*@ behavior wp_typed:
requires \separated(a, &S1, &S2); */
void assign(struct S *a);
-[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:67: Warning:
Memory model hypotheses for function 'assigns_effect':
/*@
behavior wp_typed:
@@ -186,3 +218,16 @@ Prove: IsInit_S1_S(p, a).
requires \separated(q, &S1, &S2);
*/
void assigns_effect(int *p_0, float *q, char *c, struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:76: Warning:
+ Memory model hypotheses for function 'use':
+ /*@ behavior wp_typed:
+ requires \separated(s, &S1, &S2); */
+ void use(struct S *s);
+[wp] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Memory model hypotheses for function 'chunk_typing':
+ /*@
+ behavior wp_typed:
+ requires \separated(sc, &S1, &S2);
+ requires \separated(uc, &S1, &S2);
+ */
+ void chunk_typing(unsigned char *uc, signed char *sc);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index ffca345397b95ff7963379b5e563fc3f6d562997..de7c9982adaecd3927eab97cd49cfebb8fc33069 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -1,8 +1,15 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 13 goals scheduled
+[rte] annotating function assigned_via_pointer
+[rte] annotating function assigns
+[rte] annotating function assigns_effect
+[rte] annotating function chunk_typing
+[rte] annotating function initialized_assigns
+[rte] annotating function uninitialized_assigns
+[kernel:annot:missing-spec] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Neither code nor specification for function use, generating default assigns from the prototype
+[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_lemma_fail : Unsuccess
[wp] [Qed] Goal typed_check_lemma_succeed_L1 : Valid
[wp] [Alt-Ergo] Goal typed_check_lemma_succeed_L2 : Valid
@@ -16,8 +23,10 @@
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_succeed : Valid
-[wp] Proved goals: 5 / 13
- Qed: 2
+[wp] [Qed] Goal typed_chunk_typing_assert_rte_mem_access : Valid
+[wp] [Qed] Goal typed_chunk_typing_assert_rte_mem_access_2 : Valid
+[wp] Proved goals: 7 / 15
+ Qed: 4
Alt-Ergo: 3 (unsuccess: 8)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
@@ -29,18 +38,19 @@
uninitialized_assigns - - 2 0.0%
assigned_via_pointer - - 1 0.0%
assigns_effect - 1 3 33.3%
+ chunk_typing 2 - 2 100%
------------------------------------------------------------
-[wp] tests/wp_acsl/opaque_struct.i:24: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:31: Warning:
Memory model hypotheses for function 'g':
/*@ behavior wp_typed:
requires \separated(p, &S1, &S2, &p); */
void g(void);
-[wp] tests/wp_acsl/opaque_struct.i:57: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:64: Warning:
Memory model hypotheses for function 'assign':
/*@ behavior wp_typed:
requires \separated(a, &S1, &S2); */
void assign(struct S *a);
-[wp] tests/wp_acsl/opaque_struct.i:60: Warning:
+[wp] tests/wp_acsl/opaque_struct.i:67: Warning:
Memory model hypotheses for function 'assigns_effect':
/*@
behavior wp_typed:
@@ -50,3 +60,16 @@
requires \separated(q, &S1, &S2);
*/
void assigns_effect(int *p_0, float *q, char *c, struct S *a);
+[wp] tests/wp_acsl/opaque_struct.i:76: Warning:
+ Memory model hypotheses for function 'use':
+ /*@ behavior wp_typed:
+ requires \separated(s, &S1, &S2); */
+ void use(struct S *s);
+[wp] tests/wp_acsl/opaque_struct.i:79: Warning:
+ Memory model hypotheses for function 'chunk_typing':
+ /*@
+ behavior wp_typed:
+ requires \separated(sc, &S1, &S2);
+ requires \separated(uc, &S1, &S2);
+ */
+ void chunk_typing(unsigned char *uc, signed char *sc);