diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle index f9eb09f32b6db27f54ccb7248e36e9de4d22ed19..eb6f872f382f44ed7fc83054a999d126e783b15d 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle @@ -24,6 +24,8 @@ [value] using specification for function __e_acsl_assert tests/gmp/at.i:12:[value] cannot evaluate ACSL term, \at() on a C label is unsupported tests/gmp/at.i:12:[value] warning: assertion got status unknown. +tests/gmp/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported +tests/gmp/at.i:14:[value] warning: assertion got status unknown. tests/gmp/at.i:48:[value] cannot evaluate ACSL term, \at() on a C label is unsupported tests/gmp/at.i:48:[value] warning: assertion got status unknown. tests/gmp/at.i:49:[value] cannot evaluate ACSL term, \at() on a C label is unsupported diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle index 00935cdbceb03189b6a1a4a4db4caccdbf97c825..6342f94cbdd429e15dd6309f6146fe219281938b 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle @@ -32,6 +32,8 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h:65:[value] warning: function __gmpz_init_set: precondition got status unknown. tests/gmp/at.i:12:[value] cannot evaluate ACSL term, \at() on a C label is unsupported tests/gmp/at.i:12:[value] warning: assertion got status unknown. +tests/gmp/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported +tests/gmp/at.i:14:[value] warning: assertion got status unknown. tests/gmp/at.i:48:[value] cannot evaluate ACSL term, \at() on a C label is unsupported tests/gmp/at.i:48:[value] warning: assertion got status unknown. tests/gmp/at.i:49:[value] cannot evaluate ACSL term, \at() on a C label is unsupported