diff --git a/ivette/src/dome/renderer/layout/style.css b/ivette/src/dome/renderer/layout/style.css
index ad2e376cc8c73bc870235c114fdf99da7ce10441..93af2838af18e1c13f6b0ea1f51c949f9f294f22 100644
--- a/ivette/src/dome/renderer/layout/style.css
+++ b/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);
diff --git a/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx b/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
index b8acf3ebf4e01b7387dd03956d9c82caab78211d..d82355f65ba3eab1d61670f4b99e6d1a8de1eac0 100644
--- a/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
+++ b/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> = {
diff --git a/ivette/src/frama-c/plugins/eva/components/Form.tsx b/ivette/src/frama-c/plugins/eva/components/Form.tsx
index 5137992e89f9088b1a289c5102785ddcb8e9a0a5..1b896a175b85d1b6e4aee86792cd3a96397ffad4 100644
--- a/ivette/src/frama-c/plugins/eva/components/Form.tsx
+++ b/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>
);
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index 6b5a6dbfa8b433dee7297f287049a6e426205e7d..695ba705edb8c2777d7fcb2ac9af7900bf3c93ba 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/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) {