Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • 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
  • #618

Closed
Open
Created Jan 06, 2015 by mantis-gitlab-migration@mantis-gitlab-migration

Sessions and WP do not interact properly

ID0002044: This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002044 Frama-C Plug-in > wp public 2015-01-06 2015-06-29
Reporter ploc Assigned To correnson Resolution no change required
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version -

Description :

Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!

  1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers

  2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.

  3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.

Steps To Reproduce :

Pour les points 1 et 2:

Par exemple, pour le fichier C suivant:

$ cat essai.c struct greycounter_mem {_Bool _first; };

/*@ requires \valid(self); @ ensures ((*self)._first ==1); @ assigns self;/ void greycounter_reset (struct greycounter_mem *self) { self->_first = 1;; return; }

Le script suivant active les différents problemes:

#!bin/bash src=essai.c

Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)

frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src frama-c -load session -save session -wp-prop "@assigns" $src

Error 2: no-let with why3:cvc4

frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp frama-c -load session -save session -wp-prop "@assigns" $src

Here it works

frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp frama-c -load session -save session -wp-prop "@assigns" $src

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking