[Ivette] Eva sidebar: add help icon + hide cvalue domain + style checkbox showAllFields

ivette/src/dome/renderer/layout/style.css

@@ -382,7 +382,7 @@
       background-color: var(--background-interaction);
     }
 
-    select.dome-XSelect {
+    select.dome-xSelect {
       border: none;
       min-width: 80px;
       background-color: var(--background-interaction);

ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx

@@ -102,6 +102,114 @@ export type EvaFormProps =  {[key in fieldsName]: EvaField};
 /* ************************************************************************ *
  * Option Eva Forms
  * ************************************************************************ */
+export const fieldHelp: {[key in fieldsName]: string} = {
+  "-main":
+"use <f> as entry point for analysis. See \"-lib-entry\" \n \
+if this is not for a complete application. Defaults to main",
+  "-lib-entry":
+"run analysis for an incomplete application e.g. an API call.\n \
+See the -main option to set the entry point",
+  "-eva-precision":
+"Meta-option that automatically sets up some Eva parameters\n \
+for a quick configuration of an analysis,\n \
+from 0 (fastest but rather imprecise analysis)\n \
+to 11 (accurate but potentially slow analysis).",
+  "-eva-domains": "Enable a list of analysis domains.",
+  "-eva-equality-through-calls":
+"Propagate equalities through function calls (from the caller\n \
+to the called function): none, only equalities between formal\n \
+parameters and concrete arguments, or all.",
+  "-eva-octagon-through-calls":
+"Propagate relations inferred by the octagon domain\n \
+through function calls. Disabled by default:\n \
+the octagon analysis is intra-procedural, starting\n \
+each function with an empty octagon state,\n \
+and losing the octagons inferred at the end.\n \
+The interprocedural analysis is more precise but slower.",
+  "-eva-multidim-disjunctive-invariants":
+"Try to infer structures disjunctive invariants.",
+  "-eva-auto-loop-unroll":
+"Limit of the automatic loop unrolling: all loops whose\n \
+number of iterations can be easily bounded by <n>\n \
+are completely unrolled.",
+  "-eva-min-loop-unroll":
+"Unroll <n> loop iterations for each loop, regardless of the slevel\n \
+settings and the number of states already propagated.\n \
+Can be overwritten on a case-by-case basis by loop unroll annotations.",
+  "-eva-widening-delay":
+"Do not widen before the <n>-th iteration (defaults to 3)",
+  "-eva-widening-period":
+"After the first widening, widen each <n> iterations (defaults to 2)",
+  "-eva-slevel":
+"Superpose up to <n> states when unrolling control flow.\n \
+The larger n, the more precise and expensive the analysis\n \
+(defaults to 0)",
+  "-eva-split-return":
+"Split return states of function <f> according to \
+\\result == n and \\result != n",
+  "-eva-ilevel":
+"Sets of integers are represented as sets up to <n> elements.\n \
+Above, intervals with congruence information are used\n \
+(defaults to 8, must be above 2)",
+  "-eva-plevel":
+"Use <n> as the precision level for arrays accesses.\n \
+Array accesses are precise as long as the interval for the\n \
+index contains less than n values. (defaults to 200)",
+  "-eva-partition-history":
+"Keep states distinct as long as the <n> last branching in their\n \
+traces are also distinct. (A value of 0 deactivates this feature)",
+  "-eva-subdivide-non-linear":
+"Improve precision when evaluating expressions in which a variable\n \
+appears multiple times, by splitting its value at most n times.\n \
+Defaults to 0.",
+  "-eva-alloc-builtin":
+"Select the behavior of allocation builtins.\n \
+By default, they use up to [-eva-mlevel] bases\n \
+for each callstack (<by_stack>). They can also\n \
+use one <imprecise> base for all allocations,\n \
+create a <fresh> strong base at each call,\n \
+or create a <fresh_weak> base at each call.",
+  "-eva-alloc-returns-null":
+"Memory allocation built-ins (malloc, calloc, realloc) are\n \
+modeled as nondeterministically returning a null pointer",
+  "-eva-mlevel":
+"Set to [m] the number of precise dynamic allocations\n \
+besides the initial one, for each callstack (defaults to 0)",
+  "-eva-context-depth":
+"Use <n> as the depth of the default context for Eva.\n \
+(defaults to 2)",
+  "-eva-context-width":
+"Use <n> as the width of the default context for Eva.\n \
+(defaults to 2)",
+  "-eva-context-valid-pointers":
+"Only allocate valid pointers until context-depth,\n \
+and then use NULL (defaults to false)",
+  "-warn-signed-overflow":
+"generate alarms for signed operations that overflow.",
+  "-warn-unsigned-overflow":
+"generate alarms for unsigned operations that overflow",
+  "-warn-signed-downcast":
+"generate alarms when signed downcasts may exceed the\n \
+destination range",
+  "-warn-unsigned-downcast":
+"generate alarms when unsigned downcasts may exceed the\n \
+destination range",
+  "-warn-pointer-downcast":
+"generate alarms when a pointer is converted into an integer\n \
+but may not be in the range of the destination type.",
+  "-warn-special-float":
+"generate alarms when special floats are produced: never,\n \
+only on NaN, or on infinite floats and NaN (by default).",
+  "-warn-invalid-pointer":
+"generate alarms when invalid pointers are created.",
+  "-warn-invalid-bool":
+"generate alarms when trap representations are read from\n \
+_Bool lvalues.",
+  "-warn-left-shift-negative":
+"generate alarms for signed left shifts on negative values.",
+  "-warn-right-shift-negative":
+"generate alarms for signed right shifts on negative values.",
+};
 
 export const fieldsAlwaysVisible:fieldsName[] = [
   "-main",
@@ -116,6 +224,7 @@ export const fieldsAlwaysVisible:fieldsName[] = [
 ];
 
 export const formEvaDomains: KeyVal<boolean> = {
+  'cvalue': false,
   'equality': false,
   'symbolic-locations': false,
   'octagon': false,
@@ -123,7 +232,6 @@ export const formEvaDomains: KeyVal<boolean> = {
   'multidim': false,
   'bitwise': false,
   'taint': false,
-  'cvalue': false,
 };
 
 export const formWarnSpecialFloat: KeyVal<string> = {

ivette/src/frama-c/plugins/eva/components/Form.tsx

@@ -32,6 +32,7 @@ import * as States from 'frama-c/states';
 import * as Ast from 'frama-c/kernel/api/ast';
 import * as Eva from 'frama-c/plugins/eva/api/general';
 import * as EvaDef from 'frama-c/plugins/eva/EvaDefinitions';
+import { Icon } from 'dome/controls/icons';
 
 /* -------------------------------------------------------------------------- */
 /* --- Eva form section                                                   --- */
@@ -110,11 +111,18 @@ interface EvaFormOptionsProps {
 
 function getActions<A>(
   state: Forms.FieldState<A>,
+  name: EvaDef.fieldsName,
   equal?: (a: A, b: A) => boolean,
 ): JSX.Element | undefined {
   if(!state) return undefined;
   return (
     <Forms.Actions>
+      <Icon
+        id = "HELP"
+        title = {EvaDef.fieldHelp[name]}
+        size = {12}
+        className = "eva-field-help"
+      />
       <Forms.ResetButton
         state={state}
         title="Reset"
@@ -167,6 +175,7 @@ export function EvaFormOptions(
       !showAllFields.value &&
       !EvaDef.fieldsAlwaysVisible.includes(name);
     return classes(
+      "field"+name,
       !Forms.isStable(state) && "eva-field-modified",
       notVisible ? "hidden-field" : "visible-field"
     );
@@ -183,7 +192,7 @@ export function EvaFormOptions(
       max={field.max as number}
       state={field.state as Forms.FieldState<number | undefined>}
       className={getClasses(state, name)}
-      actions={getActions(state)}
+      actions={getActions(state, name)}
       />
     );
   }
@@ -195,7 +204,7 @@ export function EvaFormOptions(
       <RadioFieldList
         fieldProps={{
           label: field.label,
-          actions: getActions(state)
+          actions: getActions(state, name)
         }}
         classeName={getClasses(state, name)}
         values={field.optionRadio as EvaDef.RadioList}
@@ -210,7 +219,7 @@ export function EvaFormOptions(
     return (
       <Forms.Field
         label={field.label}
-        actions={getActions(state)}
+        actions={getActions(state, name)}
       >
         <div className={getClasses(state, name)} />
         <Forms.ButtonField
@@ -225,7 +234,7 @@ export function EvaFormOptions(
   <Forms.SelectField
     label="Main"
     state={fields["-main"].state as Forms.FieldState<string | undefined>}
-    actions={getActions(fields["-main"].state)}
+    actions={getActions(fields["-main"].state, "-main")}
   >
     {
       fctsList.map((f) => <option
@@ -241,8 +250,9 @@ export function EvaFormOptions(
     fieldProps={{
       label: "Domains",
       actions: getActions(
-        fields["-eva-domains"]
-        .state, EvaDef.buttonListEquality)
+        fields["-eva-domains"].state,
+        "-eva-domains",
+        EvaDef.buttonListEquality)
     }}
     classeName={getClasses(fields["-eva-domains"].state, "-eva-domains")}
     state={fields["-eva-domains"].state}
@@ -285,18 +295,23 @@ export function EvaFormOptions(
         {getSpinnerField("-eva-subdivide-non-linear")}
       </Section>
 
+      {showAllFields.value &&
       <Section label="Dynamic Allocation" >
         {getRadioField("-eva-alloc-builtin")}
         {getBooleanField("-eva-alloc-returns-null")}
         {getSpinnerField("-eva-mlevel")}
       </Section>
+      }
 
+      {showAllFields.value &&
       <Section label="Initial Context" >
         {getSpinnerField("-eva-context-depth")}
         {getSpinnerField("-eva-context-width")}
         {getBooleanField("-eva-context-valid-pointers")}
       </Section>
+      }
 
+      {showAllFields.value &&
       <Section label="Alarms" >
         {getBooleanField("-warn-signed-overflow")}
         {getBooleanField("-warn-unsigned-overflow")}
@@ -309,6 +324,7 @@ export function EvaFormOptions(
         {getBooleanField("-warn-left-shift-negative")}
         {getBooleanField("-warn-right-shift-negative")}
       </Section>
+      }
 
     </Forms.SidebarForm>
   );

ivette/src/frama-c/plugins/eva/style.css

@@ -403,11 +403,16 @@ tr:first-of-type > .eva-table-callsite-box {
       border: 1px solid var(--text-discrete);
     }
 
-    input:checked { background-color: var(--positive-button-active) }
   }
 
-  .dome-xForm-field-actions { min-width: 42px; }
+  .dome-xForm-field-actions { min-width: 61px; }
+  input[type="number"]::-webkit-inner-spin-button {
+    margin-left: 4px;
+  }
   .dome-xForm-field {
+
+
+
     >input[type=radio] { display: none; }
 
     &:has(> input[type=radio]) {
@@ -443,6 +448,20 @@ tr:first-of-type > .eva-table-callsite-box {
       background-color: var(--checked-element);
       background-image: none;
     }
+
+    .field-eva-domains + button.dome-xForm-field {
+      display: none;
+    }
+  }
+
+  .dome-xForm-field-block .eva-field-help {
+    display: none;
+    background-color: var(--background-profound);
+    border-radius: 100%;
+    padding: 2px 4px;
+  }
+  .dome-xForm-field-block:hover .eva-field-help {
+    display: inline;
   }
 
   .dome-xForm-field-block:has(> .dome-xForm-field .eva-field-modified) {