@@ -200,6 +200,84 @@ The chkc juliet set of commands is used to analyze the juliet test suite cases
200200provided in
201201
202202https://github.com/static-analysis-engineering/CodeHawk-C-Targets-Juliet
203+
204+ All commands in the juliet collection of commands assume that a pointer to
205+ the location of these (pre-parsed) tests is configured in util/Config.py
206+ or in util/ConfigLocal.py. To check wheter this is the case, run
207+
208+ > chkc juliet check_config
209+
210+ It should show the analyzer configuration and the location of the juliet test
211+ case index file.
212+
213+
214+ The command
215+
216+ > chkc juliet list
217+
218+ lists the individual test cases provided with the date/time the analyzer was
219+ last run on this test, and the date/time when the results were compared with
220+ the accompanying scoring key.
221+
222+
223+ The command
224+
225+ > chkc juliet analyze <cwe> <test> (e.g., CWE121 char_type_overrun_memcpy)
226+
227+ runs the analysis on a juliet test. An individual juliet test typically
228+ consists of 18-60 files. Analysis of all of these files can be run in parallel
229+ with the optional commandline option
230+
231+ --maxprocesses <n>
232+
233+ where <n> is the number of processors to be applied.
234+
235+ A summary of the results is saved in the file summaryresults.json for later
236+ reference. Detailed results are saved in the .cch/a directory, as usual.
237+
238+
239+ The command
240+
241+ > chkc juliet analyze-sets
242+
243+ can be used to automatically run all (or a subset) of the juliet tests
244+ provided. In this case parallelism is applied to the sets, rather than to
245+ the individual files within a set.
246+
247+ The commands below can be run only on tests that have already been analyzed.
248+
249+ The command
250+
251+ > chkc juliet report <cwe> <test>
252+
253+ outputs a summary of the proof obligation analysis statistics for the given
254+ test.
255+
256+
257+ The command
258+
259+ > chkc juliet report-file <cwe> <test> <filename> (e.g., x01.c)
260+
261+ outputs the original source code annotated with the proof obligations and
262+ their analysis results for each line of code for the given source file, as well
263+ as the proof obligation analysis statistics for that source file.
264+
265+
266+ The command
267+
268+ > chkc juliet score <cwe> <test>
269+
270+ compares the analysis results the given test with the expected analysis,
271+ as provided by the scorekey.json file that comes with each test.
272+
273+
274+ The command
275+
276+ > chkc juliet investigate <cwe> <test>
277+
278+ outputs the list of open/violated/delegated proof obligations, together with
279+ their dependencies and diagnostics for the given test.
280+
203281"""
204282 print (descr )
205283 exit (0 )
@@ -384,6 +462,20 @@ def parse() -> argparse.Namespace:
384462
385463 julietanalyze .set_defaults (func = J .juliet_analyze )
386464
465+ # --- analyze-sets
466+ julietanalyzesets = julietparsers .add_parser ("analyze-sets" )
467+ julietanalyzesets .add_argument (
468+ "--maxprocesses" ,
469+ help = "maximum number of processors to use" ,
470+ type = int ,
471+ default = 1 )
472+ julietanalyzesets .add_argument (
473+ "--cwes" ,
474+ nargs = "*" ,
475+ help = "restrict analysis to these cwe's (default is all)" ,
476+ default = [])
477+ julietanalyzesets .set_defaults (func = J .juliet_analyze_sets )
478+
387479 # --- report
388480 julietreport = julietparsers .add_parser ("report" )
389481 julietreport .add_argument ("cwe" , help = "name of cwe, e.g., CWE121" )
@@ -396,7 +488,20 @@ def parse() -> argparse.Namespace:
396488 julietreportfile .add_argument ("cwe" , help = "name of cwe, e.g., CWE121" )
397489 julietreportfile .add_argument (
398490 "test" , help = "name of test case, e.g., CWE129_large" )
399- julietreportfile .add_argument ("filename" , help = "name of c file, e.g., x01.c" )
491+ julietreportfile .add_argument (
492+ "filename" , help = "name of c file, e.g., x01.c" )
493+ julietreportfile .add_argument (
494+ "--showcode" ,
495+ action = "store_true" ,
496+ help = "show the proof obligations on the code" )
497+ julietreportfile .add_argument (
498+ "--open" ,
499+ action = "store_true" ,
500+ help = "show only open proof obligations on the code" )
501+ julietreportfile .add_argument (
502+ "--showinvariants" ,
503+ action = "store_true" ,
504+ help = "show invariants for open proof obligations" )
400505 julietreportfile .set_defaults (func = J .juliet_report_file )
401506
402507 # --- score
@@ -420,6 +525,47 @@ def parse() -> argparse.Namespace:
420525
421526 julietscore .set_defaults (func = J .juliet_score )
422527
528+ # --- investigate
529+ julietinvestigate = julietparsers .add_parser ("investigate" )
530+ julietinvestigate .add_argument ("cwe" , help = "name of cwe, e.g., CWE121" )
531+ julietinvestigate .add_argument (
532+ "test" , help = "name of test case, e.g., CWE129_large" )
533+ julietinvestigate .add_argument (
534+ "--xdelegated" ,
535+ help = "exclude delegated proof obligations" ,
536+ action = "store_true" )
537+ julietinvestigate .add_argument (
538+ "--xviolated" ,
539+ help = "exclude violated proof obligations" ,
540+ action = "store_true" )
541+ julietinvestigate .add_argument (
542+ "--predicates" ,
543+ nargs = "*" ,
544+ help = "predicates of interest (default: all)" ,
545+ default = [])
546+ julietinvestigate .set_defaults (func = J .juliet_investigate )
547+
548+ # --- report-requests
549+ julietreprequests = julietparsers .add_parser ("report-requests" )
550+ julietreprequests .add_argument ("cwe" , help = "name of cwe, e.g., CWE121" )
551+ julietreprequests .add_argument (
552+ "test" , help = "name of test case, e.g., CWE129_large" )
553+ julietreprequests .set_defaults (func = J .juliet_report_requests )
554+
555+ # --- dashboard
556+ julietdashboard = julietparsers .add_parser ("dashboard" )
557+ julietdashboard .add_argument (
558+ "--cwe" , help = "only report results on the given cwe" )
559+ julietdashboard .add_argument (
560+ "--variant" , help = "only report results on the given variant" )
561+ julietdashboard .set_defaults (func = J .juliet_dashboard )
562+
563+ # --- project-dashboard
564+ julietpdashboard = julietparsers .add_parser ("project-dashboard" )
565+ julietpdashboard .add_argument (
566+ "--cwe" , help = "only report results on the given cwe" )
567+ julietpdashboard .set_defaults (func = J .juliet_project_dashboard )
568+
423569 # --------------------------------------------------------------- c-file ---
424570 cfilecmd = subparsers .add_parser ("c-file" )
425571 cfilecmd .set_defaults (func = cfilecommand )
0 commit comments