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 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1621
Closed
Open
Created Sep 30, 2009 by Dillon Pariente@dillon

Problem with is_finite predicate generated by -val

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


Id Project Category View Due Date Updated
ID0000259 Frama-C Plug-in > Eva public 2009-09-30 2014-02-12
Reporter dpariente Assigned To pascal Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version Frama-C Carbon-20101201-beta1

Description :

Launching: frama-c foo.c with foo.c (generated by "frama-c -val" on the original code) containing:

/* Generated by Frama-C / double f(double a , double b ) { double t ; t = 0.0; /@ assert \is_finite("+", a, b); // synthesized assert \is_finite("*", a+b, a-b); // synthesized assert \is_finite("-", a, b); // synthesized */ t = (a + b) * (a - b); return (t); }

yields: foo.c:13:[kernel] user error: syntax error while parsing annotation

which seems to be due to multiple asserts in the same @-comment.

Please note also that once the 3 asserts are 'exploded' into their own @-comment, then "frama-c foo.c" displays: foo.c:13:[kernel] user error: Error during annotations analysis: no such predicate or logic function \is_finite(char *, double , double ) (but this very last point was already discussed in other threads). Kernel seems to wait for a double typed expression parameter in \is_finite predicate, doesn't it? Like this single assert: //@ assert \is_finite((double)((a + b) * (a - b)));

Regards, Dillon

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