Skip to content
Snippets Groups Projects
Normal view Permalink
bts1304.res.oracle 409 B
Newer Older
Julien Signoles's avatar
[E-ACSL] faster initialization of the dataflow analysis  
Julien Signoles committed
1 
[e-acsl] beginning translation.
Andre Maroneze's avatar
synchronize with frama-c/frama-c!1112  
Andre Maroneze committed
2 
FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
Julien Signoles's avatar
[E-ACSL] faster initialization of the dataflow analysis  
Julien Signoles committed
3 
[e-acsl] translation done in project "e-acsl".
Julien Signoles's avatar
[tests] remove 'COMMENT: no diff' lines from bts and e-acsl-runtime tests  
Julien Signoles committed
4 
tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
Kostyantyn Vorobyov's avatar
Adjusted test suite as per changes of RTL prefixes  
Kostyantyn Vorobyov committed
5 
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.