Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2580

Closed
Open
Created Oct 20, 2021 by Raul Monti@raulmonti

Non ghost lvalue when assigning array (frama-c 22)

The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines //@ ghost int acopy[len]; and //@ ghost acopy[i] = a[i];. I am wondering if this is actually not allowed or if it is just a bug?

Regards, Raúl Monti.

#include <stdio.h>

/*@ requires len >= 0;
  @ requires \valid(a+(0..len-1));
  @*/
void add1(int* a, int len) {
    //@ ghost int acopy[len];
    int i;
    for(i = 0; i < len; i++) {
        //@ ghost acopy[i] = a[i];
    }
    for(i = 0; i < len; i++) {
        a[i] = a[i] + 1;
    }
    //@ assert \forall integer i; 0 <= i < len ==> a[i] == acopy[i] + 1;
}

int main() {
    int a[3];
    a[0] = 0;
    a[1] = 1;
    a[2] = 2;
    add1(a, 3);
    return 0;
}

The output I get when running e-acsl-gcc.sh add.c -c -O add in frama-c-22:

e-acsl-gcc.sh add.c -c -O add
+ frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64  -no-frama-c-stdlib add.c -e-acsl -e-acsl-share=.../.opam/default/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing add.c (with preprocessing)
[kernel:ghost:bad-use] add.c:7: Warning: 
  Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] add.c:10: Warning: 
  '*(acopy + i)' is a non-ghost lvalue, it cannot be assigned in ghost code
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking