Rename exp.precious_globs and clarify what it does

[michael-schwarz]

The documentation currently says

reg Experimental "exp.precious_globs"    "[]"    "Global variables that should be handled flow-sensitively when using earlyglobs."

However, Simmo discovered that "precious globs" are also "my favorite things" that exclude things from invalidation:

analyzer/src/analyses/base.ml

Lines 1799 to 1803 in 85536ab

	let my_favorite_things = List.map Json.string !precious_globs in
	let is_fav_addr x =
	List.exists (fun x -> List.mem x.vname my_favorite_things) (AD.to_var_may x)
	in
	let invalids' = List.filter (fun (x,_,_) -> not (is_fav_addr x)) invalids in

So one should rethink what precious_globs are, give them a sensible name, and describe their behavior.

---

Also, we should rename exp.extraspecials to something that better describes what it means

;reg Experimental "exp.extraspecials"     "[]"    "List of functions that must be analyzed as unknown extern functions"

[sim642]

exp.extraspecials just adds functions to "special" (which isn't a good name in itself) functions in LibraryFunctions. We should also reevaluate the default "special" functions:

analyzer/src/analyses/libraryFunctions.ml

Line 462 in 85536ab

let lib_funs = ref (Set.String.of_list ["list_empty"; "__raw_read_unlock"; "__raw_write_unlock"; "spinlock_check"; "spin_trylock"; "spin_unlock_irqrestore"])

In #183 I already had to remove some, because apparently LDV benchmarks in SV-COMP had some custom definitions for a few of those and that was changing the behavior. Of course the whole library functions thing needs to be redone, but these default (and unremovable with any options!) "specials" can really shoot in the foot and are safer removed (and added to just the tests/programs that need them).