Commit ac707065 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'bugfix/basile/eacsl-128-variadic-compat' into 'master'

[eacsl][variadic] Fix variadic compilability and eacsl compatibility

Closes e-acsl#128

See merge request frama-c/frama-c!2886
parents eade128e e882d048
......@@ -321,20 +321,3 @@ ML_LINT_KO+=src/plugins/value_types/precise_locs.ml
ML_LINT_KO+=src/plugins/value_types/value_types.ml
ML_LINT_KO+=src/plugins/value_types/value_types.mli
ML_LINT_KO+=src/plugins/value_types/widen_type.ml
ML_LINT_KO+=src/plugins/variadic/classify.ml
ML_LINT_KO+=src/plugins/variadic/environment.ml
ML_LINT_KO+=src/plugins/variadic/extends.ml
ML_LINT_KO+=src/plugins/variadic/extends.mli
ML_LINT_KO+=src/plugins/variadic/format_parser.ml
ML_LINT_KO+=src/plugins/variadic/format_parser.mli
ML_LINT_KO+=src/plugins/variadic/format_pprint.ml
ML_LINT_KO+=src/plugins/variadic/format_string.ml
ML_LINT_KO+=src/plugins/variadic/format_typer.ml
ML_LINT_KO+=src/plugins/variadic/format_typer.mli
ML_LINT_KO+=src/plugins/variadic/format_types.mli
ML_LINT_KO+=src/plugins/variadic/generic.ml
ML_LINT_KO+=src/plugins/variadic/options.ml
ML_LINT_KO+=src/plugins/variadic/standard.ml
ML_LINT_KO+=src/plugins/variadic/translate.ml
ML_LINT_KO+=src/plugins/variadic/va_build.ml
ML_LINT_KO+=src/plugins/variadic/va_types.mli
......@@ -17,6 +17,9 @@
Open Source Release <next-release>
##################################
- Variadic [2020-10-14] Don't print generated function name but print
original name and a comment with the generated name so that the
printed code is compilable.
- Aorai [2020-10-13] Ya automata can set auxiliary variables during a
transition, and use such variables in subsequent guards.
- Kernel [2020-10-09] Add option -print-config-json, to output Frama-C
......
......@@ -1454,6 +1454,8 @@ src/plugins/variadic/generic.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/replacements.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/replacements.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/standard.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/translate.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/va_build.ml: CEA_LGPL_OR_PROPRIETARY
......
......@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
- E-ACSL [2020-10-14] Add Support for Variadic generated functions in
the AST (frama-c/e-acsl#128).
- E-ACSL [2020-10-06] Add support for the `\separated` predicate.
(frama-c/e-acsl#31)
-* E-ACSL [2020-10-06] Fix a soundness bug when translating a range with a
......
......@@ -763,8 +763,7 @@ LDFLAGS="$OPTION_LDFLAGS"
# Extra Frama-C Flags E-ACSL needs
FRAMAC_FLAGS="$FRAMAC_FLAGS \
-remove-unused-specified-functions \
-variadic-no-translation"
-remove-unused-specified-functions"
# C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
......
......@@ -639,6 +639,9 @@ let inject_in_global (env, main) = function
env, main
| g when Rtl.Symbols.mem_global g ->
env, main
(* generated function declaration: nothing to do *)
| GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
env, main
(* variable declarations *)
| GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
......
......@@ -36,6 +36,9 @@ let is_fc_or_compiler_builtin vi =
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
let is_fc_stdlib_generated vi =
Cil.hasAttribute "fc_stdlib_generated" vi.vattr
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
......
......@@ -40,6 +40,10 @@ val result_vi: kernel_function -> varinfo
val is_fc_or_compiler_builtin: varinfo -> bool
val is_fc_stdlib_generated: varinfo -> bool
(** Returns true if the [varinfo] is a generated stdlib function. (For instance
generated function by the Variadic plug-in. *)
val term_addr_of: loc:location -> term_lval -> typ -> term
val cty: logic_type -> typ
......
......@@ -42,12 +42,14 @@ let generate_code =
Temporal.enable (Options.Temporal_validity.get ());
if Plugin.is_present "variadic" then begin
let opt_name = "-variadic-translation" in
if Dynamic.Parameter.Bool.get opt_name () then begin
if Dynamic.Parameter.Bool.get opt_name () &&
Options.Validate_format_strings.get () then begin
if Ast.is_computed () then
Options.abort
"The variadic translation must be turned off for E-ACSL. \
Please use option '-variadic-no-translation'";
Options.warning "deactivating variadic translation";
"The variadic translation is incompatible with E-ACSL option \
'%s'.@ Please use option '-variadic-no-translation'."
Options.Validate_format_strings.option_name
Options.warning "deactivating variadic translation";
Dynamic.Parameter.Bool.off opt_name ();
end
end;
......
......@@ -392,6 +392,8 @@ let must_duplicate kf vi =
not (is_variadic_function vi)
&& (* it is not a built-in *)
not (Misc.is_fc_or_compiler_builtin vi)
&& (* it is not a generated function *)
not (Misc.is_fc_stdlib_generated vi)
&&
((* either explicitely listed as to be not instrumented *)
not (Functions.instrument kf)
......
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
......@@ -26,7 +26,7 @@ int main(void)
int i = 1;
t[0] = 1;
t[1] = 2;
printf(__gen_e_acsl_literal_string,x,t[0],t[i]);
printf(__gen_e_acsl_literal_string,x,t[0],t[i]); /* printf_va_1 */
__retres = 0;
__e_acsl_memory_clean();
return __retres;
......
STDOPT: #"-e-acsl-validate-format-strings"
STDOPT: #"-variadic-no-translation -e-acsl-validate-format-strings"
MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking
MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation
MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/constructor.c:16: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
......@@ -7,7 +7,7 @@ char *__gen_e_acsl_literal_string;
void f(void) __attribute__((__constructor__));
void f(void)
{
printf(__gen_e_acsl_literal_string);
printf(__gen_e_acsl_literal_string); /* printf_va_1 */
char *buf = malloc((unsigned long)10 * sizeof(char));
free((void *)buf);
return;
......@@ -36,7 +36,7 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
printf(__gen_e_acsl_literal_string_2);
printf(__gen_e_acsl_literal_string_2); /* printf_va_2 */
__retres = 0;
__e_acsl_memory_clean();
return __retres;
......
......@@ -40,7 +40,8 @@ int main(int argc, char const **argv)
int t = 0;
UP: ;
if (t == 2) {
printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string);
printf(__gen_e_acsl_literal_string_2,t,
(char *)__gen_e_acsl_literal_string); /* printf_va_1 */
goto RET;
}
AGAIN:
......@@ -58,7 +59,8 @@ int main(int argc, char const **argv)
}
/*@ assert \valid(&a); */ ;
if (t == 2) {
printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_3);
printf(__gen_e_acsl_literal_string_2,t,
(char *)__gen_e_acsl_literal_string_3); /* printf_va_2 */
__e_acsl_delete_block((void *)(& a));
goto UP;
}
......@@ -74,7 +76,8 @@ int main(int argc, char const **argv)
"tests/memory/local_goto.c",36);
}
/*@ assert \valid(&b); */ ;
printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4);
printf(__gen_e_acsl_literal_string_2,t,
(char *)__gen_e_acsl_literal_string_4); /* printf_va_3 */
__e_acsl_delete_block((void *)(& a));
__e_acsl_delete_block((void *)(& b));
goto AGAIN;
......
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] beginning translation.
[e-acsl] tests/special/e-acsl-instrument.c:58: Warning:
ignoring effect of variadic function vol
[e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/special/e-acsl-instrument.c:43: Warning:
Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/special/e-acsl-instrument.c:44: Warning:
Neither code nor specification for function __builtin_va_arg, generating default assigns from the prototype
[eva:alarm] tests/special/e-acsl-instrument.c:44: Warning:
accessing uninitialized left-value.
assert \initialized(&tmp);
(tmp from vararg)
......@@ -4,12 +4,6 @@
#include "stdio.h"
extern int __e_acsl_sound_verdict;
/* compiler builtin:
void __builtin_va_arg(__builtin_va_list, unsigned long, void *); */
/* compiler builtin:
void __builtin_va_end(__builtin_va_list); */
/* compiler builtin:
void __builtin_va_start(__builtin_va_list); */
int __gen_e_acsl_uninstrument1(int *p);
int uninstrument1(int *p)
......@@ -68,17 +62,22 @@ int instrument2(int *p)
return __retres;
}
int vol(int n , ...)
int vol(int n, void * const *__va_params)
{
int __retres;
va_list vl;
int tmp;
__builtin_va_start(vl,n);
tmp = __builtin_va_arg (vl, int);
/*@ assert Eva: initialization: \initialized(&tmp); */
__e_acsl_store_block((void *)(& vl),(size_t)8);
__e_acsl_store_block((void *)(& __va_params),(size_t)8);
__e_acsl_full_init((void *)(& vl));
vl = __va_params;
tmp = *((int *)*vl);
__e_acsl_full_init((void *)(& vl));
vl ++;
int r = tmp;
__builtin_va_end(vl);
__retres = 0;
__e_acsl_delete_block((void *)(& __va_params));
__e_acsl_delete_block((void *)(& vl));
return __retres;
}
......@@ -113,7 +112,17 @@ int main(void)
57);
}
/*@ assert \initialized(&y); */ ;
tmp = vol(6,1);
{
int __va_arg0 = 1;
__e_acsl_store_block((void *)(& __va_arg0),(size_t)4);
__e_acsl_full_init((void *)(& __va_arg0));
void *__va_args[1] = {& __va_arg0};
__e_acsl_store_block((void *)(__va_args),(size_t)8);
__e_acsl_full_init((void *)(& __va_args));
tmp = vol(6,(void * const *)(__va_args));
__e_acsl_delete_block((void *)(& __va_arg0));
__e_acsl_delete_block((void *)(__va_args));
}
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
__e_acsl_memory_clean();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment