Lines Matching refs:parser
35 # The C parser emits variables with a suffix to indicate their types; this lets
36 # the C parser distinguish `char x` from `int x`.
38 # The suffix map should match the C parser types for `uint{8,16,32,64}_t` in
2661 parser = optparse.OptionParser()
2662 parser.add_option('--c_defs', action='store_true', default=False)
2663 parser.add_option('--environment', action='store', default='sel4',
2665 parser.add_option('--hol_defs', action='store_true', default=False)
2666 parser.add_option('--hol_proofs', action='store_true', default=False)
2667 parser.add_option('--sorry_lemmas', action='store_true',
2669 parser.add_option('--prune', action='append',
2671 parser.add_option('--toplevel', action='append',
2673 parser.add_option('--umm_types', action='store',
2675 parser.add_option('--multifile_base', action='store', default=None)
2676 parser.add_option('--cspec-dir', action='store', default=None,
2678 parser.add_option('--thy-output-path', action='store', default=None,
2680 parser.add_option('--skip_modifies', action='store_true', default=False)
2681 parser.add_option('--showclasses', action='store_true', default=False)
2682 parser.add_option('--debug', action='store_true', default=False)
2684 options, args = parser.parse_args()
2701 parser.error("'cspec_dir' not defined.")
2706 parser.error("Theory output path was not specified")
2708 parser.error(
2713 parser.error('--umm_types must be specified when generating HOL proofs')
2715 del parser