rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
53 stars 28 forks source link

[CN] `cn verify` silently ignores multiple files #527

Open thatplguy opened 3 months ago

thatplguy commented 3 months ago

Problem

cn verify f1.c f2.c will attempt to verify f2.c and ignore f1.c.

Expected behavior

Either require that exactly one file be listed on the command line and fail otherwise, or attempt to verify all files.

How to reproduce

CN version: git-b73624664 [2024-08-21 18:11:18 -0700]

f1.c

void bad()
/*@ ensures 0i32 == 1i32; @*/
{}

f2.c

void good() {}

CLI command

# The following command succeeds, which implies that f1.c is verified.
cn verify f1.c f2.c

Output

# Functions from f1.c are not listed in the results, which IMO is too subtle to 
# indicate that f1.c was not analyzed.
[1/1]: good -- pass
septract commented 3 months ago

To fix this we probably should update the file definition in Common_flags / main.ml to follow this approach: https://github.com/mjambon/cmdliner-cheatsheet?tab=readme-ov-file#any-number-of-anonymous-arguments-defaulting-to-non-empty-list