diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle index bd90eaf199bc57cab2f4b64fea7a1d14bd12f043..db7d99e671c08bdc8eb7d5c58870f1883377fe21 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle @@ -2,11 +2,11 @@ [e-acsl] warning: annotating undefined function `strlen': the generated program may miss memory instrumentation if there are memory-related annotations. -FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. +FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. Ignoring annotation. -FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. +FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -FRAMAC_SHARE/libc/string.h:90:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported. +FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -37,12 +37,12 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown. [value] using specification for function __initialized tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc); tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time -FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. [value] using specification for function strlen -FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown. -FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates +FRAMAC_SHARE/libc/string.h:91:[value] Function strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates [value] using specification for function __delete_block -FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown. +FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown. tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle index 52e0b30ccc7e7884bcbb52285cceec21b63bb0cf..d3b2a7b1d26620c85beacd090db3d66dc331e57e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle @@ -6,7 +6,7 @@ tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `logic func Ignoring annotation. tests/e-acsl-runtime/mainargs.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -FRAMAC_SHARE/libc/string.h:90:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported. +FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". [value] Analyzing a complete application starting at main @@ -61,12 +61,12 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown. [value] using specification for function __initialized tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc); tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time -FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. [value] using specification for function strlen -FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown. -FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates +FRAMAC_SHARE/libc/string.h:91:[value] Function strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates [value] using specification for function __delete_block -FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown. +FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown. tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time