diff --git a/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx b/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
index 487acdaf77885f7c40e14d8398d717f8d6c954a2..b8acf3ebf4e01b7387dd03956d9c82caab78211d 100644
--- a/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
+++ b/ivette/src/frama-c/plugins/eva/EvaDefinitions.tsx
@@ -53,23 +53,39 @@ export interface ButtonFieldListProps {
}
export type fieldsName =
- "precision" |
- "main" |
- "libEntry" |
- "domains" |
- "iLevel" |
- "WideningDelay" |
- "ArrayPrecisionLevel" |
- "LinearLevel" |
- "EqualityCall" |
- "OctagonCall" |
- "sLevel" |
- "MinLoopUnroll" |
- "AutoLoopUnroll" |
- "HistoryPartitioning" |
- "SplitReturn" |
- "AllocReturnsNull" |
- "WarnPointerComparison"
+ "-main" |
+ "-lib-entry" |
+ "-eva-precision" |
+ "-eva-domains" |
+ "-eva-equality-through-calls" |
+ "-eva-octagon-through-calls" |
+ "-eva-multidim-disjunctive-invariants" |
+ "-eva-auto-loop-unroll" |
+ "-eva-min-loop-unroll" |
+ "-eva-widening-delay" |
+ "-eva-widening-period" |
+ "-eva-slevel" |
+ "-eva-split-return" |
+ "-eva-ilevel" |
+ "-eva-plevel" |
+ "-eva-partition-history" |
+ "-eva-subdivide-non-linear" |
+ "-eva-alloc-builtin" |
+ "-eva-alloc-returns-null" |
+ "-eva-mlevel" |
+ "-eva-context-depth" |
+ "-eva-context-width" |
+ "-eva-context-valid-pointers" |
+ "-warn-signed-overflow" |
+ "-warn-unsigned-overflow" |
+ "-warn-signed-downcast" |
+ "-warn-unsigned-downcast" |
+ "-warn-pointer-downcast" |
+ "-warn-special-float" |
+ "-warn-invalid-pointer" |
+ "-warn-invalid-bool" |
+ "-warn-left-shift-negative" |
+ "-warn-right-shift-negative"
export interface EvaField {
label: string,
@@ -86,32 +102,17 @@ export type EvaFormProps = {[key in fieldsName]: EvaField};
/* ************************************************************************ *
* Option Eva Forms
* ************************************************************************ */
-export const fieldsPrecisionDependent: fieldsName[] = [
- "MinLoopUnroll",
- "AutoLoopUnroll",
- "WideningDelay",
- "HistoryPartitioning",
- "sLevel",
- "iLevel",
- "ArrayPrecisionLevel",
- "LinearLevel",
- "domains",
- "SplitReturn",
- "EqualityCall",
- "OctagonCall"
-];
export const fieldsAlwaysVisible:fieldsName[] = [
- "precision",
- "main",
- "libEntry",
- "domains",
- "sLevel",
- "iLevel",
- "AutoLoopUnroll",
- "SplitReturn",
- "AllocReturnsNull",
- "WarnPointerComparison",
+ "-main",
+ "-lib-entry",
+ "-eva-precision",
+ "-eva-domains",
+ "-eva-auto-loop-unroll",
+ "-eva-slevel",
+ "-eva-split-return",
+ "-eva-partition-history",
+ "-eva-ilevel",
];
export const formEvaDomains: KeyVal<boolean> = {
@@ -119,26 +120,37 @@ export const formEvaDomains: KeyVal<boolean> = {
'symbolic-locations': false,
'octagon': false,
'gauges': false,
+ 'multidim': false,
+ 'bitwise': false,
+ 'taint': false,
'cvalue': false,
};
+
+export const formWarnSpecialFloat: KeyVal<string> = {
+ 'none': 'None',
+ 'nan': 'NaN',
+ 'non-finite': 'NonFinite',
+};
+
export const formEvaSplitReturn: KeyVal<string> = {
'': 'None',
'full': 'Full',
'auto': 'Auto'
};
-export const formEvaPointerComparison: KeyVal<string> = {
- '': 'None',
- 'pointer': 'Pointer',
- 'all': 'All'
-};
-
export const formEvaEqualityCall: KeyVal<string> = {
'none': 'None',
'formals': 'Formals',
'all': 'All'
};
+export const formEvaAllocBuiltin: KeyVal<string> = {
+ 'imprecise': 'Imprecise',
+ 'by_stack': 'ByStack',
+ 'fresh': 'Fresh',
+ 'fresh_weak': 'FreshWeak',
+};
+
export const domainsToKeyVal = (value: string): KeyVal<boolean> => {
const domains = { ...formEvaDomains };
const array = value.split(',');
diff --git a/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx b/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx
index 93ff242072c8beacbb3a0fa4c41ce69eae292d0f..abf5f9ef9f602069aaf5cbf7fac5d587f3bb05f1 100644
--- a/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx
+++ b/ivette/src/frama-c/plugins/eva/EvaSidebar.tsx
@@ -37,9 +37,10 @@ export function EvaSideBar(): JSX.Element {
return Forms.useBuffer(remote, useServerField(state, defaultValue));
}
- const precision = useField(Params.evaPrecision, 0);
const main = useField(Params.main, "");
const libEntry = useField(Params.libEntry, false);
+ const precision = useField(Params.evaPrecision, 0);
+
const domains = useField(Params.evaDomains, "cvalue");
const domainsFiltered = Forms.useFilter(
domains,
@@ -47,101 +48,192 @@ export function EvaSideBar(): JSX.Element {
EvaDef.KeyValToDomains,
EvaDef.formEvaDomains
);
- const WideningDelay = useField(Params.evaWideningDelay, 0);
- const ArrayPrecisionLevel = useField(Params.evaPlevel, 0);
- const LinearLevel = useField(Params.evaSubdivideNonLinear, 0);
const EqualityCall = useField(Params.evaEqualityThroughCalls, "none");
const OctagonCall = useField(Params.evaOctagonThroughCalls, false);
- const sLevel = useField(Params.evaSlevel, 0);
- const iLevel = useField(Params.evaIlevel, 0);
+ const MultidimDisjunctive =
+ useField(Params.evaMultidimDisjunctiveInvariants, false);
+
const AutoLoopUnroll = useField(Params.evaAutoLoopUnroll, 0);
const MinLoopUnroll = useField(Params.evaMinLoopUnroll, 0);
+ const WideningDelay = useField(Params.evaWideningDelay, 0);
+ const WideningPeriod = useField(Params.evaWideningPeriod, 0);
+
+ const sLevel = useField(Params.evaSlevel, 0);
const SplitReturn = useField(Params.evaSplitReturn, "none");
- const HistoryPartitioning = useField(Params.evaPartitionHistory, 0);
+ const PartitionHistory = useField(Params.evaPartitionHistory, 0);
+
+ const iLevel = useField(Params.evaIlevel, 0);
+ const pLevel = useField(Params.evaPlevel, 0);
+ const Subdivide = useField(Params.evaSubdivideNonLinear, 0);
+
+ const AllocBuiltin = useField(Params.evaAllocBuiltin, "");
const AllocReturnsNull = useField(Params.evaAllocReturnsNull, false);
- const WarnPointerComparison =
- useField(Params.evaWarnUndefinedPointerComparison, "none");
+ const mLevel = useField(Params.evaMlevel, 0);
- const evaFields = {
- "precision": {
- label: "Precision",
- step: 1, min: -1, max: 11,
- state: precision
- },
- "main": {
+ const ContextDepth = useField(Params.evaContextDepth, 0);
+ const ContextWidth = useField(Params.evaContextWidth, 0);
+ const ContextValidPointers = useField(Params.evaContextValidPointers, false);
+
+ const warnSignedOverflow = useField(Params.warnSignedOverflow, true);
+ const warnUnsignedOverflow = useField(Params.warnUnsignedOverflow, false);
+ const warnSignedDowncast = useField(Params.warnSignedDowncast, false);
+ const warnUnsignedDowncast = useField(Params.warnUnsignedDowncast, false);
+ const warnPointerDowncast = useField(Params.warnPointerDowncast, true);
+ const warnSpecialFloat = useField(Params.warnSpecialFloat, "non-finite");
+ const warnInvalidPointer = useField(Params.warnInvalidPointer, false);
+ const warnInvalidBool = useField(Params.warnInvalidBool, true);
+ const warnLeftShiftNegative = useField(Params.warnLeftShiftNegative, true);
+ const warnRightShiftNegative = useField(Params.warnRightShiftNegative, false);
+
+ const evaFields : EvaDef.EvaFormProps = {
+ "-main": {
label: "Main",
state: main
},
- "libEntry": {
+ "-lib-entry": {
label: "LibEntry",
state: libEntry
},
- "domains": {
+ "-eva-precision": {
+ label: "Precision",
+ step: 1, min: -1, max: 11,
+ state: precision
+ },
+ "-eva-domains": {
label: "Domains",
state: domainsFiltered
},
- "sLevel": {
- label: "Slevel",
- step: 100, min: 0, max: 5000,
- state: sLevel
+ "-eva-equality-through-calls": {
+ label: "Equality through function call",
+ optionRadio: EvaDef.formEvaEqualityCall,
+ state: EqualityCall
},
- "iLevel": {
- label: "Ilevel",
- step: 10, min: 0, max: 256,
- state: iLevel
+ "-eva-octagon-through-calls": {
+ label: "Octagon through function call",
+ state: OctagonCall
},
- "AutoLoopUnroll": {
- label: "Auto loop unroll",
- step: 50, min: 0, max: 1024,
+ "-eva-multidim-disjunctive-invariants": {
+ label: "Multidim disjunctive invariant inference",
+ state: MultidimDisjunctive
+ },
+ "-eva-auto-loop-unroll": {
+ label: "Automatic loop unrolling",
+ step: 20, min: 0, max: 1024,
state: AutoLoopUnroll
},
- "SplitReturn": {
+ "-eva-min-loop-unroll": {
+ label: "Minimun loop unrolling",
+ step: 1, min: 0, max: 10,
+ state: MinLoopUnroll
+ },
+ "-eva-widening-delay": {
+ label: "Widening delay",
+ step: 1, min: 1, max: 10,
+ state: WideningDelay
+ },
+ "-eva-widening-period": {
+ label: "Widening period",
+ step: 1, min: 1, max: 10,
+ state: WideningPeriod
+ },
+ "-eva-slevel": {
+ label: "Slevel",
+ step: 10, min: 0, max: 10000,
+ state: sLevel
+ },
+ "-eva-split-return": {
label: "Split return",
optionRadio: EvaDef.formEvaSplitReturn,
state: SplitReturn
},
- "AllocReturnsNull": {
- label: "Alloc returns null",
+ "-eva-ilevel": {
+ label: "Ilevel",
+ step: 10, min: 0, max: 1024,
+ state: iLevel
+ },
+ "-eva-plevel": {
+ label: "PLevel",
+ step: 100, min: 0, max: 5000,
+ state: pLevel
+ },
+ "-eva-partition-history": {
+ label: "History partitioning",
+ step: 1, min: 0, max: 5,
+ state: PartitionHistory
+ },
+ "-eva-subdivide-non-linear": {
+ label: "Subdivision on non-linear expressions",
+ step: 20, min: 0, max: 1024,
+ state: Subdivide
+ },
+ "-eva-alloc-builtin": {
+ label: "Allocation builtin behavior",
+ optionRadio: EvaDef.formEvaAllocBuiltin,
+ state: AllocBuiltin
+ },
+ "-eva-alloc-returns-null": {
+ label: "Allocation return null",
state: AllocReturnsNull
},
- "WarnPointerComparison": {
- label: "Warn pointer comparison",
- optionRadio: EvaDef.formEvaPointerComparison,
- state: WarnPointerComparison
+ "-eva-mlevel": {
+ label: "Mlevel",
+ step: 1, min: 0, max: 20,
+ state: mLevel
},
- "MinLoopUnroll": {
- label: "Min loop unroll",
- step: 1, min: 0, max: 4,
- state: MinLoopUnroll
+ "-eva-context-depth": {
+ label: "Initial context depth",
+ step: 1, min: 0, max: 10,
+ state: ContextDepth
},
- "WideningDelay": {
- label: "Widening delay",
- step: 1, min: 1, max: 6,
- state: WideningDelay
+ "-eva-context-width": {
+ label: "Initial context width",
+ step: 1, min: 1, max: 1024,
+ state: ContextWidth
},
- "HistoryPartitioning": {
- label: "History partitioning",
- step: 1, min: 0, max: 2,
- state: HistoryPartitioning
+ "-eva-context-valid-pointers": {
+ label: "Validity of initial pointers",
+ state: ContextValidPointers
},
- "ArrayPrecisionLevel": {
- label: "PLevel",
- step: 100, min: 0, max: 5000,
- state: ArrayPrecisionLevel
+ "-warn-signed-overflow": {
+ label: "Signed overflow",
+ state: warnSignedOverflow
},
- "LinearLevel": {
- label: "Linear level",
- step: 5, min: 0, max: 220,
- state: LinearLevel
+ "-warn-unsigned-overflow": {
+ label: "Unsigned overflow",
+ state: warnUnsignedOverflow
},
- "EqualityCall": {
- label: "Equality call",
- optionRadio: EvaDef.formEvaEqualityCall,
- state: EqualityCall
+ "-warn-signed-downcast": {
+ label: "Signed downcast",
+ state: warnSignedDowncast
},
- "OctagonCall": {
- label: "Octagon call",
- state: OctagonCall
+ "-warn-unsigned-downcast": {
+ label: "Unsigned downcast",
+ state: warnUnsignedDowncast
+ },
+ "-warn-pointer-downcast": {
+ label: "Pointer downcast",
+ state: warnPointerDowncast
+ },
+ "-warn-special-float": {
+ label: "Special float",
+ optionRadio: EvaDef.formWarnSpecialFloat,
+ state: warnSpecialFloat
+ },
+ "-warn-invalid-pointer": {
+ label: "Invalid pointer",
+ state: warnInvalidPointer
+ },
+ "-warn-invalid-bool": {
+ label: "Invalid _Bool",
+ state: warnInvalidBool
+ },
+ "-warn-left-shift-negative": {
+ label: "Negative left shift",
+ state: warnLeftShiftNegative
+ },
+ "-warn-right-shift-negative": {
+ label: "Negative right shift",
+ state: warnRightShiftNegative
},
};
diff --git a/ivette/src/frama-c/plugins/eva/components/Form.tsx b/ivette/src/frama-c/plugins/eva/components/Form.tsx
index f188f4369a7359cb3fa40758a5daf6c6afb6cc23..5137992e89f9088b1a289c5102785ddcb8e9a0a5 100644
--- a/ivette/src/frama-c/plugins/eva/components/Form.tsx
+++ b/ivette/src/frama-c/plugins/eva/components/Form.tsx
@@ -103,6 +103,7 @@ export function RadioFieldList(
/* -------------------------------------------------------------------------- */
/* ---Eva Form --- */
/* -------------------------------------------------------------------------- */
+
interface EvaFormOptionsProps {
fields: EvaDef.EvaFormProps;
}
@@ -162,13 +163,11 @@ export function EvaFormOptions(
state: Forms.FieldState<A>,
name: EvaDef.fieldsName
): string | undefined {
- const isDepPrecision = EvaDef.fieldsPrecisionDependent.includes(name);
const notVisible =
!showAllFields.value &&
!EvaDef.fieldsAlwaysVisible.includes(name);
return classes(
!Forms.isStable(state) && "eva-field-modified",
- isDepPrecision && "eva-precision-dep",
notVisible ? "hidden-field" : "visible-field"
);
}
@@ -213,7 +212,7 @@ export function EvaFormOptions(
label={field.label}
actions={getActions(state)}
>
- <div className={getClasses(state, "libEntry")} />
+ <div className={getClasses(state, name)} />
<Forms.ButtonField
label={state.value ? "Enabled" : "disabled"}
state={state}
@@ -224,14 +223,14 @@ export function EvaFormOptions(
const mainField =
<Forms.SelectField
- label="Eva main"
- state={fields["main"].state as Forms.FieldState<string | undefined>}
- actions={getActions(fields["main"].state)}
+ label="Main"
+ state={fields["-main"].state as Forms.FieldState<string | undefined>}
+ actions={getActions(fields["-main"].state)}
>
{
fctsList.map((f) => <option
key={f.key} id={f.key} value={f.name}
- className={getClasses(fields["main"].state, "main")}
+ className={getClasses(fields["-main"].state, "-main")}
>{f.name}</option>
)
}
@@ -241,10 +240,12 @@ export function EvaFormOptions(
<ButtonFieldList
fieldProps={{
label: "Domains",
- actions: getActions(fields["domains"].state, EvaDef.buttonListEquality)
+ actions: getActions(
+ fields["-eva-domains"]
+ .state, EvaDef.buttonListEquality)
}}
- classeName={getClasses(fields["domains"].state, "domains")}
- state={fields["domains"].state}
+ classeName={getClasses(fields["-eva-domains"].state, "-eva-domains")}
+ state={fields["-eva-domains"].state}
/>;
return (
@@ -257,31 +258,56 @@ export function EvaFormOptions(
disabled={isNoAlwaysVisibleFieldsStable()}
/>
- {getSpinnerField("precision")}
{mainField}
- {getBooleanField("libEntry")}
+ {getBooleanField("-lib-entry")}
+ {getSpinnerField("-eva-precision")}
+
+ <Section label="Analysis Domains" >
+ {domainsField}
+ {getRadioField("-eva-equality-through-calls")}
+ {getBooleanField("-eva-octagon-through-calls")}
+ {getBooleanField("-eva-multidim-disjunctive-invariants")}
+ </Section>
+
+ <Section label="Analysis of Loops" >
+ {getSpinnerField("-eva-auto-loop-unroll")}
+ {getSpinnerField("-eva-min-loop-unroll")}
+ {getSpinnerField("-eva-widening-delay")}
+ {getSpinnerField("-eva-widening-period")}
+ </Section>
+
+ <Section label="Partitioning and Disjunctions" >
+ {getSpinnerField("-eva-slevel")}
+ {getRadioField("-eva-split-return")}
+ {getSpinnerField("-eva-partition-history")}
+ {getSpinnerField("-eva-ilevel")}
+ {getSpinnerField("-eva-plevel")}
+ {getSpinnerField("-eva-subdivide-non-linear")}
+ </Section>
- <Section label="Abstract interpretation" >
- {domainsField}
- {getSpinnerField("iLevel")}
- {getSpinnerField("WideningDelay")}
- {getSpinnerField("ArrayPrecisionLevel")}
- {getSpinnerField("LinearLevel")}
- {getRadioField("EqualityCall")}
- {getBooleanField("OctagonCall")}
+ <Section label="Dynamic Allocation" >
+ {getRadioField("-eva-alloc-builtin")}
+ {getBooleanField("-eva-alloc-returns-null")}
+ {getSpinnerField("-eva-mlevel")}
</Section>
- <Section label="State partitioning" >
- {getSpinnerField("sLevel")}
- {getSpinnerField("MinLoopUnroll")}
- {getSpinnerField("AutoLoopUnroll")}
- {getSpinnerField("HistoryPartitioning")}
- {getRadioField("SplitReturn")}
+ <Section label="Initial Context" >
+ {getSpinnerField("-eva-context-depth")}
+ {getSpinnerField("-eva-context-width")}
+ {getBooleanField("-eva-context-valid-pointers")}
</Section>
- <Section label="Message" >
- {getBooleanField("AllocReturnsNull")}
- {getRadioField("WarnPointerComparison")}
+ <Section label="Alarms" >
+ {getBooleanField("-warn-signed-overflow")}
+ {getBooleanField("-warn-unsigned-overflow")}
+ {getBooleanField("-warn-signed-downcast")}
+ {getBooleanField("-warn-unsigned-downcast")}
+ {getBooleanField("-warn-pointer-downcast")}
+ {getRadioField("-warn-special-float")}
+ {getBooleanField("-warn-invalid-pointer")}
+ {getBooleanField("-warn-invalid-bool")}
+ {getBooleanField("-warn-left-shift-negative")}
+ {getBooleanField("-warn-right-shift-negative")}
</Section>
</Forms.SidebarForm>