fix(yaml): extend crab yaml by using sea_base.yaml

seahorn/sea_crab_base.yaml

@@ -1,47 +1,9 @@
 verify_options:
-# Optimization level
-  '-O3': ''
-# 
-# PREPROCESSING
-#
-  inline: ''
-  enable-loop-idiom: ''
-  enable-indvar: ''
-  no-lower-gv-init-struct: ''
-  externalize-addr-taken-functions: ''
-  no-kill-vaarg: ''
-  with-arith-overflow: true
   horn-unify-assumes: false
-# do not instrument library functions with memory assertions 
-  no-fat-fns: 'bcmp,memcpy,assert_bytes_match,ensure_linked_list_is_allocated,sea_aws_linked_list_is_valid'
   horn-gsa: false
-# context-sensitive type-aware alias analysis 
-  dsa: sea-cs-t
-# weak support for function pointers. sea-dsa is better but less stable
-  devirt-functions: 'types'
-# bit-precise memory-precise operational semantics
-  bmc: opsem
-  horn-vcgen-use-ite: ''
 # ignore control flow
   horn-vcgen-only-dataflow: false
 # reduce by data dependence
   horn-bmc-coi: false
-# static allocator supports symbolic allocation size
-  sea-opsem-allocator: static
-# stack allocation from a symbolic starting point
-  horn-explicit-sp0: false
-# lambdas for memory
-  horn-bv2-lambdas: false
-# use z3 simplifier during vcgen
-  horn-bv2-simplify: true
-# wide memory manager to track pointer sizes
-  horn-bv2-extra-widemem: ''
-# intermediate results in human readable form for debugging
-  '-S': ''
-# keep intermediate results for debugging 
-  keep-temps: ''
-  temp-dir: /tmp/verify-c-common
-# time and result stats
-  horn-stats: true
   horn-bv2-crab-lower-is-deref: ''
   horn-bmc-crab-dom: 'zones'

verify.py.in

@@ -92,10 +92,7 @@ def main(argv):
                    'yama', '--yforce']
 
             # base config
-            if args.crab:
-                base_config = os.path.join(script_dir, 'seahorn', 'sea.crab.yaml')
-            else:
-                base_config = os.path.join(script_dir, 'seahorn', 'sea.yaml')
+            base_config = os.path.join(script_dir, 'seahorn', 'sea.yaml')
             if args.cex:
                 base_config = os.path.join(script_dir, 'seahorn',
                                            'sea.cex.yaml')
@@ -106,6 +103,12 @@ def main(argv):
                 vac_config = os.path.join(script_dir, 'seahorn',
                                           'sea.vac.yaml')
                 cmd.extend(['-y', vac_config])
+
+            # Crab in Opsem config
+            if args.crab:
+                crab_config = os.path.join(script_dir, 'seahorn', 
+                                          'sea.crab.yaml')
+                cmd.extend(['-y', crab_config])
 
             # pcond config
             if args.pcond: