Frama-C Bug Tracking System - Frama-C
View Issue Details
0002432Frama-CKernelpublic2019-03-20 17:272019-07-05 11:41
Stevendeo 
virgile 
lowminoralways
closedfixed 
Frama-C 18-Argon 
Frama-C 19-Potassium 
0002432: Attributes of size 1 are rejected
Attributes are parsed by Extlib.strip_underscore that removes underscores before and after a string. However, the function always returns an empty string when the size of the input is 1. The attribute is then rejected.
The error is not raised in Chlorine.
frama-c foo.c
Here is a possible bug fix

let strip_underscore s =
  let l = String.length s in
  if l = 1
  then
    match s with
      "_" -> ""
    | _ -> s
  else
    let rec start i =
      if i >= l then l-1
      else if s.[i] = '_' then start (i + 1) else i
    in
    let st = start 0 in
    if st = l - 1 then ""
    else begin
      let rec finish i =
        (* We know that we will stop at >= st >= 0 *)
        if s.[i] = '_' then finish (i - 1) else i
      in
      let fin = finish (l - 1) in
      String.sub s st (fin - st + 1)
    end
No tags attached.
c foo.c (52) 2019-03-20 17:27
https://bts.frama-c.com/file_download.php?file_id=1307&type=bug
Issue History
2019-03-20 17:27StevendeoNew Issue
2019-03-20 17:27StevendeoFile Added: foo.c
2019-04-09 17:27virgileNote Added: 0006762
2019-04-09 17:28virgileStatusnew => resolved
2019-04-09 17:28virgileFixed in Version => Frama-C 19-Potassium
2019-04-09 17:28virgileResolutionopen => fixed
2019-04-09 17:28virgileAssigned To => virgile
2019-07-05 11:41signolesStatusresolved => closed

Notes
(0006762)
virgile   
2019-04-09 17:27   
Actually, the main issue is returning l-1 when no non-underscore character is found. It should return l (and the test for emptiness be updated accordingly). This is fixed in dev branch and will appear in the next Frama-C release. Thanks for the report.