diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx index 19313c95f70dcaef7d82de6746604d12a9626032..b5b8470ca51e964073d0b2d70c54f56163b8944b 100644 --- a/ivette/src/frama-c/kernel/Properties.tsx +++ b/ivette/src/frama-c/kernel/Properties.tsx @@ -83,6 +83,10 @@ function newFilter( const DEFAULTS: { [key: string]: IFilterContent } = { 'currentScope': newFilter(false, "Current scope"), + /** source */ + 'source.alarms': newFilter(true, "Alarms"), + 'source.libc': newFilter(true, "Libc specifications"), + 'source.others': newFilter(true, "Others"), /** status */ 'status.valid': newFilter(true, "Valid"), 'status.valid_hyp': newFilter(true, "Valid under hyp."), @@ -109,9 +113,6 @@ const DEFAULTS: { [key: string]: IFilterContent } = { 'kind.pragma': newFilter(true, "Pragma"), 'kind.assumes': newFilter(true, "Assumes"), 'kind.others': newFilter(true, "Others"), - /** source */ - 'source.alarms': newFilter(true, "Alarms"), - 'source.others': newFilter(true, "Others"), /** alarms */ 'alarms.overflow': newFilter(true, "Overflows"), 'alarms.division_by_zero': newFilter(true, "Divisions by zero"), @@ -248,31 +249,37 @@ function filterKind( } } +function filterSource(p: Property): boolean { + const condAlarms = Boolean(p.alarm); + const condLibc = p.from_libc; + const others = Boolean(!condAlarms && !condLibc); + + return (filter('source.libc') || !condLibc) + && (filter('source.alarms') || !condAlarms) + && (filter('source.others') || !others); +} + function filterAlarm(alarm: string | undefined): boolean { - if (alarm) { - if (!filter('source.alarms')) return false; - switch (alarm) { - case 'overflow': return filter('alarms.overflow'); - case 'division_by_zero': return filter('alarms.division_by_zero'); - case 'mem_access': return filter('alarms.mem_access'); - case 'index_bound': return filter('alarms.index_bound'); - case 'pointer_value': return filter('alarms.pointer_value'); - case 'shift': return filter('alarms.shift'); - case 'ptr_comparison': return filter('alarms.ptr_comparison'); - case 'differing_blocks': return filter('alarms.differing_blocks'); - case 'separation': return filter('alarms.separation'); - case 'overlap': return filter('alarms.overlap'); - case 'initialization': return filter('alarms.initialization'); - case 'dangling_pointer': return filter('alarms.dangling_pointer'); - case 'is_nan_or_infinite': - case 'is_nan': return filter('alarms.special_float'); - case 'float_to_int': return filter('alarms.float_to_int'); - case 'function_pointer': return filter('alarms.function_pointer'); - case 'bool_value': return filter('alarms.bool_value'); - default: return false; - } + switch (alarm) { + case 'overflow': return filter('alarms.overflow'); + case 'division_by_zero': return filter('alarms.division_by_zero'); + case 'mem_access': return filter('alarms.mem_access'); + case 'index_bound': return filter('alarms.index_bound'); + case 'pointer_value': return filter('alarms.pointer_value'); + case 'shift': return filter('alarms.shift'); + case 'ptr_comparison': return filter('alarms.ptr_comparison'); + case 'differing_blocks': return filter('alarms.differing_blocks'); + case 'separation': return filter('alarms.separation'); + case 'overlap': return filter('alarms.overlap'); + case 'initialization': return filter('alarms.initialization'); + case 'dangling_pointer': return filter('alarms.dangling_pointer'); + case 'is_nan_or_infinite': + case 'is_nan': return filter('alarms.special_float'); + case 'float_to_int': return filter('alarms.float_to_int'); + case 'function_pointer': return filter('alarms.function_pointer'); + case 'bool_value': return filter('alarms.bool_value'); + default: return true; } - return filter('source.others'); } function filterEva(p: Property): boolean { @@ -515,7 +522,7 @@ class PropertyModel extends Arrays.CompactModel<PropKey, Property> { const current = this.filterScope; const filtering = current && filter('currentScope'); const filterScope = filtering ? prop.scope === current : true; - return filterScope && filterProperty(prop); + return filterScope && filterSource(prop) && filterProperty(prop); } } @@ -611,11 +618,11 @@ function PropertyFilter(): JSX.Element { const getCheckBox = (type: TFilterType): JSX.Element => { return <> { - Object.entries(DEFAULTS) - .filter(([key, ]) => key.startsWith(type+".")) - .map(([key, elt]) => - <CheckField key={key} label={elt.label} path={key} title={elt.title}/> - ) + Object.entries(DEFAULTS) + .filter(([key, ]) => key.startsWith(type+".")) + .map(([key, elt]) => + <CheckField key={key} label={elt.label} path={key} title={elt.title}/> + ) }</>; }; @@ -628,9 +635,7 @@ function PropertyFilter(): JSX.Element { className="properties-section-names" infos={Form.isValid(namesState.error) && namesState.value.length >= 2 ? "Active" : ""} summary={!Form.isValid(namesState.error) ? - <IconButton icon='WARNING' kind="warning" title={`Errors in section`}/> - : undefined - } + <Icon id='WARNING' kind="warning" title={`Errors in section`}/> : undefined } > <Form.TextField label={""} @@ -641,9 +646,9 @@ function PropertyFilter(): JSX.Element { /> </Section> + <FilterSection label="Source" prefix="source"> { getCheckBox("source") } </FilterSection> <FilterSection label="Status" prefix="status" unfold> { getCheckBox("status") } </FilterSection> <FilterSection label="Property kind" prefix="kind"> { getCheckBox("kind") } </FilterSection> - <FilterSection label="Source" prefix="source"> { getCheckBox("source") } </FilterSection> <FilterSection label="Alarms kind" prefix="alarms"> { getCheckBox("alarms") } </FilterSection> <FilterSection label="Eva"> { getCheckBox("eva") } </FilterSection> </Scroll> diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml index bba21be7666385e9fa90760540a5d5b2eccdf427..a90a5d57013f3a68e6c759dcd5a8ebefd2137c6a 100644 --- a/src/plugins/server/kernel_properties.ml +++ b/src/plugins/server/kernel_properties.ml @@ -248,6 +248,13 @@ let find_alarm = function | Property.IPCodeAnnot annot -> Alarms.find annot.ica_ca | _ -> None +let is_libc ip = + match Property.source ip with + | None -> false + | Some position -> + let libc_path = Kernel.Share.get_dir "libc" in + Filepath.is_relative ~base_name:libc_path position.pos_path + let model = States.model () let () = States.column model ~name:"descr" @@ -289,6 +296,11 @@ let () = States.column model ~name:"source" ~data:(module Kernel_ast.Position) ~get:(fun ip -> Property.location ip |> fst) +let () = States.column model ~name:"from_libc" + ~descr:(Md.plain "Is the property from the Frama-C libc?") + ~data:(module Jbool) + ~get:is_libc + let () = States.column model ~name:"alarm" ~descr:(Md.plain "Alarm name (if the property is an alarm)") ~data:(module Joption(Jstring))