check-invariant option doesn't exist anymore but is still in the help file

[polgreen]

The check-invariant cmdline option is in the help file of goto-instrument and isn't actually implemented. Not sure if it got removed at some point or was never implemented.

CBMC version: 5.12 (cbmc-5.12-d8598f8-1417-gcccdfd9ba)
Operating system: MacOS

The command line option --check-invariant function instruments invariant checking function\n" is outputted when i run goto-instrument --help, but, as far as I can tell, it's not implemented in the code base anywhere. Trying to run goto-instrument with this command line option just results in goto-instrument outputting the help file.

I didgit grep check-invariant and it returns only the help file, so I don't think this cmdline option is actually implemented

goto-instrument/goto_instrument_parse_options.cpp:    " --check-invariant function   instruments invariant checking function\n"

Exact command line resulting in the issue: goto-instrument --check-invariant function file.gb
What behaviour did you expect: I don't know, but it should at least be a valid command line option
What happened instead: outputted the help file.

[martin-cs]

Ooops! I wish I could say I was surprised but ... Want to write the patch to remove it or should I?

[polgreen]

I'll remove it

I don't suppose anyone remembers if this code ever existed and what it did though/how it did it though?

[martin-cs]

On Fri, 2020-02-07 at 16:57 -0800, E Polgreen wrote: I'll remove it I don't suppose anyone remembers if this code ever existed and what it did though/how it did it though?

git blame suggests that the person to ask is Daniel in 2012. IIRC there was a project that finished around then with University of Manchester and Airbus that used some kind of contracts on code sections. Possibly it was for that? If not then I think 2012 is around the start of goto-instrument as a separate tool and towards the end of satabs being alive so maybe the plan was to move over some of the code from that?