Commit b4567b26 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/andre/vla-generate-spec' into 'master'

sync with frama-c/frama-c!1756

See merge request frama-c/e-acsl!205
parents 92910ea2 59118376
......@@ -400,11 +400,12 @@ void apply_specifier(char *format, int spec)
return;
}
/*@ assigns \nothing; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *);
/*@ assigns \nothing;
frees p; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *p);
/* compiler builtin:
void *__builtin_alloca(unsigned long); */
__attribute__((__FC_BUILTIN__)) void *__builtin_alloca(unsigned long size); */
void test_specifier_application(char const *allowed, char const *fmt,
int only_negative, char *at)
{
......
......@@ -18,8 +18,6 @@ tests/format/printf.c:88:[kernel] warning: Floating-point constant 0.2 is not re
FRAMAC_SHARE/libc/stdio.h:157:[kernel:annot:missing-spec] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/unistd.h:781:[kernel:annot:missing-spec] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel:annot:missing-spec] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
FRAMAC_SHARE/libc/string.h:319:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
......
......@@ -2,11 +2,12 @@
#include "stdio.h"
#include "stdlib.h"
int LEN = 10;
/*@ assigns \nothing; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *);
/*@ assigns \nothing;
frees p; */
__attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *p);
/* compiler builtin:
void *__builtin_alloca(unsigned long); */
__attribute__((__FC_BUILTIN__)) void *__builtin_alloca(unsigned long size); */
int main(int argc, char **argv)
{
int __retres;
......
[e-acsl] beginning translation.
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/vla.c:8:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/vla.c:12:[value:alarm] warning: assertion got status invalid (stopping propagation).
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