Skip to content
Snippets Groups Projects
  • David Bühler's avatar
    b2b8be59
    [Eva] Splits the downcast test into 5 runs. Also tests -no-warn-pointer-downcast. · b2b8be59
    David Bühler authored
    Run 0 tests the default configuration of Frama-C: no downcast alarms, except
    for pointers.
    Runs 1 to 3 correspond to the previous run with successive -then, and test:
    - emission of signed downcast alarms (option -warn-signed-downcast)
    - emission of unsigned downcast alarms (option -warn-unsigned-downcast)
    - the relaxed semantics of the Eva option -eva-warn-signed-converted-downcast
    Run 4 disables all downcast alarms, including downcast of pointer values.
    b2b8be59
    History
    [Eva] Splits the downcast test into 5 runs. Also tests -no-warn-pointer-downcast.
    David Bühler authored
    Run 0 tests the default configuration of Frama-C: no downcast alarms, except
    for pointers.
    Runs 1 to 3 correspond to the previous run with successive -then, and test:
    - emission of signed downcast alarms (option -warn-signed-downcast)
    - emission of unsigned downcast alarms (option -warn-unsigned-downcast)
    - the relaxed semantics of the Eva option -eva-warn-signed-converted-downcast
    Run 4 disables all downcast alarms, including downcast of pointer values.