diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml index c837a3ede6ba819838292be5010ca9f7178ac395..f67f603fc98175edf595cf440088ee7a915e7427 100644 --- a/src/plugins/wp/cfgAnnot.ml +++ b/src/plugins/wp/cfgAnnot.ml @@ -247,13 +247,17 @@ module CallContract = WpContext.StaticGenerator(Kernel_function) List.iter (add wpost @@ mk_post Normal) bhv.b_post_cond ; List.iter (add wexit @@ mk_post Exits) bhv.b_post_cond ; end behaviors ; + let assigns = match assigns_upper_bound behaviors with + | WritesAny -> WritesAny + | Writes froms -> Writes (normalize_froms Normal froms) + in { contract_cond = List.rev !wcond ; contract_hpre = List.rev !whpre ; contract_post = List.rev !wpost ; contract_exit = List.rev !wexit ; contract_smoke = [] ; - contract_assigns = assigns_upper_bound behaviors + contract_assigns = assigns } end) diff --git a/src/plugins/wp/tests/wp_acsl/old-assigns.c b/src/plugins/wp/tests/wp_acsl/old-assigns.c new file mode 100644 index 0000000000000000000000000000000000000000..d15399639e4e6ddafb364f535c3d8535e84f40c9 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/old-assigns.c @@ -0,0 +1,12 @@ +#include <string.h> + +/*@ assigns dest[0..strlen{Old}(src)]; @*/ +void strcpy_OLD(char *restrict dest, const char *restrict src); + +/*@ + requires \separated(dest+(0..), src+(0..)); + assigns dest[0..strlen(src)]; +*/ +void old(char *dest, const char *src) { + strcpy_OLD(dest, src); +} diff --git a/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..568225a6abd60a8d0d3b36d2b450b4aa2a16a6e9 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle/old-assigns.res.oracle @@ -0,0 +1,19 @@ +# frama-c -wp [...] +[kernel] Parsing tests/wp_acsl/old-assigns.c (with preprocessing) +[wp] Running WP plugin... +[wp] Warning: Missing RTE guards +------------------------------------------------------------ + Function old +------------------------------------------------------------ + +Goal Assigns (file tests/wp_acsl/old-assigns.c, line 8) in 'old': +Call Effect at line 11 +Prove: true. + +------------------------------------------------------------ + +Goal Assigns (file tests/wp_acsl/old-assigns.c, line 8) in 'old': +Call Effect at line 11 +Prove: true. + +------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..9d6f20338598c338f7b64b88a6c313dc66cf3596 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/old-assigns.res.oracle @@ -0,0 +1,13 @@ +# frama-c -wp [...] +[kernel] Parsing tests/wp_acsl/old-assigns.c (with preprocessing) +[wp] Running WP plugin... +[wp] Warning: Missing RTE guards +[wp] 2 goals scheduled +[wp] [Qed] Goal typed_old_assigns_exit : Valid +[wp] [Qed] Goal typed_old_assigns_normal : Valid +[wp] Proved goals: 2 / 2 + Qed: 2 +------------------------------------------------------------ + Functions WP Alt-Ergo Total Success + old 2 - 2 100% +------------------------------------------------------------